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

A Day of Invited Talks

There is no call for contributions.

Thu 22 Jun

dsw-2017-papers
09:00 - 10:00: DSW 2017 - Intro & industry perspective on crypto at Vertex WS216
Chair(s): Andrew Appel
dsw-2017-papers149811480000009:00 - 09:15
Day opening
dsw-2017-papers149811570000009:15 - 10:00
Talk
dsw-2017-papers
10:30 - 12:10: DSW 2017 - Academic crypto projects; industry perspective on formal-methods integration at Vertex WS216
Chair(s): Zhong Shao
dsw-2017-papers149812020000010:30 - 11:00
Talk
dsw-2017-papers149812200000011:00 - 11:30
Talk
dsw-2017-papers149812380000011:30 - 12:10
Talk
dsw-2017-papers
13:40 - 15:00: DSW 2017 - Academic C-verification project; industry perspective on hypervisors at Vertex WS216
Chair(s): Adam Chlipala
dsw-2017-papers149813160000013:40 - 14:20
Talk
dsw-2017-papers149813400000014:20 - 15:00
Talk
dsw-2017-papers
15:30 - 17:00: DSW 2017 - Academic hypervisor project; closing discussion at Vertex WS216
Chair(s): Lennart Beringer
dsw-2017-papers149813820000015:30 - 16:15
Talk
dsw-2017-papers149814090000016:15 - 17:00
Day closing