Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Agenda
Time  Event 
9:00-10:00  

Invited talk: Verifying Transformations of the LLVM IR

Steve Zdancewic (University of Pennsylvania) 

10:00-10:30 Morning break 
10:30-11:00  

Compilation using abstract machines for game semantics

Olle Fredriksson Read abstract

11:00-11:30  

Approximate reasoning for Markov Processes

Radu Mardare and Prakash Panangaden Read abstract

11:30-12:00  

Monad-based Partial Correctness Assertions

Sergey Goncharov and Lutz Schroder Read abstract

12:00-14:00   Lunch 
14:00-15:00  

Invited talk: Machine code, formal verification and functional programming

Magnus Myreen (University of Cambridge) 

15:00-15:30  

Towards Verified Shared-memory Cooperation for C

Lennart Beringer, Gordon Stewart, Robert Dockins and Andrew W. Appel Read abstract

15:30-16:00   Afternoon break 
16:00-16:30  

Low-Level Program Verification using Matching Logic Reachability

Dwight Guth, Andrei Stefanescu and Grigore Rosu Read abstract

16:30-17:00  

Memory Trace Oblivious Program Execution

Chang Liu, Michael Hicks and Elaine Shi Read abstract