PLDI, ECOOP, Curry On, DEBS, LCTES and ISMM (series) / PLDI 2017 (series) / DSW 2017 (series) / Deep Specifications in the Wild 2017 /
Introduction to verification using the VST
Thu 22 Jun 2017 11:00 - 11:30 at Vertex WS216 - Academic crypto projects; industry perspective on formal-methods integration Chair(s): Zhong Shao
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 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
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 30mTalk | Correct-by-Construction Generation of Fast Code for Elliptic Curves DSW Adam Chlipala Massachusetts Institute of Technology, USA | ||
11:00 30mTalk | Introduction to verification using the VST DSW Lennart Beringer Princeton University | ||
11:30 40mTalk | Using formal tools to develop high-assurance software for autonomous ground vehicles DSW Aleksey Nogin HRL Laboratories, LLC | ||
