University College London

file

Visible to the public Separation Logic Modulo Theories

Submitted by TimTh on Tue, 05/28/2013 - 11:51am. Contributor:

Presented as part of the 2013 HCSS conference.

ABSTRACT:

file

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

Submitted by TimTh on Tue, 05/14/2013 - 1:15pm. Contributors:

ABSTRACT

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.