j.alglave@ucl.ac.uk

Lecturer, PPLV group

Reorder Workshop

I organise Reorder, associated with CAV. Consider submitting!

Publications

• Partial Orders for Efficient Bounded Model Checking of Concurrent Software (in CAV 2013)
• Software Verification for Weak Memory via Program Transformation (in ESOP 2013)
• A Formal Hierarchy of Weak Memory Models (in FMSD 2012, Volume 41, Number 2)
• An Axiomatic Memory Model for Power Multiprocessors (in CAV 2012)
• Synchronising C/C++ and Power (in PLDI 2012)
• Fences in Weak Memory Models (Extended Version) (journal version of CAV 2010, in FMSD 2012, Volume 40, Number 2)
• Soundness of Data Flow Analyses for Weak Memory Models (in APLAS 2011)
• Making Software Verification Tools Really Work (invited paper, in ATVA 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 EC² 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

• CBMC: an extension of CBMC that handles weak memory via partial orders.
• Coq development associated to the ESOP 2013 paper
• goto-instrument: a tool for transforming a C program so that the transformed program's SC executions are all the executions the initial program could have on a weak architecture.
• 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 and FMSD 2012 papers

Ph.D. Thesis

Here is the manuscript.

818 Pumpkin

• C'est bon la salade !
• J'aime le mardi !
• Ceci n'est pas la page web de Samuel Mimram.