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

10:30 - 12:10: DSW 2017 - Academic crypto projects; industry perspective on formal-methods integration at Vertex WS216
Chair(s): Zhong ShaoYale University
dsw-2017-papers10:30 - 11:00
Adam ChlipalaMassachusetts Institute of Technology, USA
dsw-2017-papers11:00 - 11:30
Lennart BeringerPrinceton University
dsw-2017-papers11:30 - 12:10
Aleksey NoginHRL Laboratories, LLC