University College London


Visible to the public Separation Logic Modulo Theories

Presented as part of the 2013 HCSS conference.



Visible to the public Verification of Concurrent Software in the Context of Weak Memory


Multiprocessors are now so widespread that verification cannot ignore any longer the flavor of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.