Write a Blog >>

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 Jun
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:40 - 15:00: DSW 2017 - Academic C-verification project; industry perspective on hypervisors at Vertex WS216
Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA
dsw-2017-papers13:40 - 14:20
Andrew AppelPrinceton
dsw-2017-papers14:20 - 15:00
Michael TautschnigAmazon Web Services