Write a Blog >>

DeepSpec is a 5-year, 4-institution initiative to push forward the state of the art in applying computer proof assistants to verify realistic software and hardware stacks at scale. A key part of the mission is to engage with industry, learning about adoption obstacles, educating practitioners about how to apply these techniques, and even launching pilot collaborations with specific companies. For that reason, we want to bring together academics and industrial engineers to discuss the low-hanging fruit of particular formal tools that are ready for tech transfer.

What makes the proposed workshop different from a research conference is its focus on particular ideas and artifacts that industry should be able to start experimenting with in the next year or two. What makes the proposed workshop different from a developer conference is that we are willing to consider technology investments (in formal methods, in particular) that may take years to pay off, but which seem promising to deliver significant increases in assurance levels and/or significant decreases in development costs.

List of Presentations

A detailed schedule will appear soon, with more information on talks and speakers, but here is the plan as of now.

Invited Speakers from Industry

Speakers From the DeepSpec Project

While the industry speakers represent a variety of formal-methods approaches, the presentations from our team will all be about work done with the Coq proof assistant.

Presentations

Title
Building Faith in Experts: Applying Formal Verification to Cryptography
DSW
CertiKOS: A Breakthrough toward Hacker-Resistant Operating Systems
DSW
Challenges in Analysing Virtualisation Stacks
DSW
Closing discussion
DSW

Correct-by-Construction Generation of Fast Code for Elliptic Curves
DSW
Introduction to DeepSpec
DSW
Introduction to verification using the VST
DSW
Using formal tools to develop high-assurance software for autonomous ground vehicles
DSW
Verifying concurrent C programs with the Verified Software Toolchain
DSW

A Day of Invited Talks

There is no call for contributions.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Thu 22 Jun

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

09:00 - 10:00
Intro & industry perspective on cryptoDSW at Vertex WS216
Chair(s): Andrew W. Appel Princeton
09:00
15m
Day opening
Introduction to DeepSpec
DSW
Lennart Beringer Princeton University, Adam Chlipala Massachusetts Institute of Technology, USA
09:15
45m
Talk
Building Faith in Experts: Applying Formal Verification to Cryptography
DSW
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
13:40 - 15:00
Academic C-verification project; industry perspective on hypervisorsDSW at Vertex WS216
Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA
13:40
40m
Talk
Verifying concurrent C programs with the Verified Software Toolchain
DSW
Andrew W. Appel Princeton
14:20
40m
Talk
Challenges in Analysing Virtualisation Stacks
DSW
Michael Tautschnig Amazon Web Services
15:30 - 17:00
Academic hypervisor project; closing discussionDSW at Vertex WS216
Chair(s): Lennart Beringer Princeton University
15:30
45m
Talk
CertiKOS: A Breakthrough toward Hacker-Resistant Operating Systems
DSW
Zhong Shao Yale University
16:15
45m
Day closing
Closing discussion
DSW