Write a Blog >>

The Verified Software Toolchain is a higher-order impredicative concurrent separation logic for C, proven sound in Coq w.r.t. CompCert Clight. The Floyd proof automation is a collection of definitions and proof tactics to support concrete program verification using forward symbolic execution. The talk will present a user-oriented introduction to the system, including outlines of a number of illustrative examples and case studies.

Thu 22 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Academic crypto projects; industry perspective on formal-methods integrationDSW at Vertex WS216
Chair(s): Zhong Shao Yale University
10:30
30m
Talk
Correct-by-Construction Generation of Fast Code for Elliptic Curves
DSW
Adam Chlipala Massachusetts Institute of Technology, USA
11:00
30m
Talk
Introduction to verification using the VST
DSW
Lennart Beringer Princeton University
11:30
40m
Talk
Using formal tools to develop high-assurance software for autonomous ground vehicles
DSW
Aleksey Nogin HRL Laboratories, LLC