Write a Blog >>

It is well understood that many cyber-physical systems incorporate software that is getting increasingly complex, hard to manage, and therefore often quite fragile. We will present our recent work on addressing this challenge using formal methods based tools and techniques for creation of software for cyber-physical systems that provide strong assurances that the resulting software would be secure, safe, and reliable.

These include - the use of a formally verified operating system; - the use of a toolchain where proofs of controller safety properties in a theorem prover for hybrid systems are used for synthesis of high assurance high performance control code implementations; - leveraging general-purpose formal tools to create automated synthesizers for high assurance message handling code that comes with proofs of correctness (which imply absence of misbehaviors due to e.g. malformed messages); and - tools for producing high assurance and medium assurance glue code that links different modules in a secure safe and resilient manner.

This talk will primarily present a tool user perspective – outlining how we applied these tools and describing both successes and challenges of this effort.

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
Correct-by-Construction Generation of Fast Code for Elliptic Curves
Adam Chlipala Massachusetts Institute of Technology, USA
Introduction to verification using the VST
Lennart Beringer Princeton University
Using formal tools to develop high-assurance software for autonomous ground vehicles
Aleksey Nogin HRL Laboratories, LLC