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 Jun
|13:40 - 14:20|
|14:20 - 15:00|
Michael TautschnigAmazon Web Services