Jade Alglave
|
Jade Alglave
|
Publications
- Soundness of Data Flow Analyses for Weak Memory Models (in APLAS 2011)
- Stability in Weak Memory Models (in CAV 2011)
- Understanding Power Multiprocessors (in PLDI 2011)
- Litmus: Running Tests Against Hardware (in TACAS 2011)
- Fences in Weak Memory Models (in CAV 2010)
- Relaxed Memory Models Must Be Rigorous (in EC2 2010)
- The Semantics of x86-CC Multiprocessor Machine Code (in POPL 2009)
- The Semantics of Power and ARM Multiprocessor Machine Code (in DAMP 2009)
Software
- offence: a tool for enforcing stability to x86 and Power assembly programs, i.e. the program has nothing but SC executions.
- Coq development associated to the CAV 2011 paper
- diy: a tool suite for generating and running tests in PowerPC and x86 assembly against hardware.
- Coq development associated to the CAV 2010 paper
Ph.D. Thesis
-
Here is the manuscript.
Teaching
-
I was lecturing Software Verification during Hilary term 2011, with the help of many people.