Verifying concurrent C programs with the Verified Software Toolchain
VST’s program logic, Verifiable C, is a concurrent separation logic. You can use it to verify the functional correctness (not just safety!) of shared-memory C programs (in the Pthreads style). Of course, most shared-memory programs have lots of sequential programming too. I’ll demonstrate how Verifiable C supports the interactive verification of both sequential and parallel code.
Thu 22 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:40 - 15:00
|Verifying concurrent C programs with the Verified Software Toolchain
Andrew W. Appel Princeton
|Challenges in Analysing Virtualisation Stacks
Michael Tautschnig Amazon Web Services