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.
Program Display Configuration
Thu 22 Jun
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Viennachange
13:40 - 15:00
Academic C-verification project; industry perspective on hypervisorsDSW at Vertex WS216 Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA
