Deep Specifications

Formal verification of systems software requires specifications that are:

  • rich (describing complex component behaviors in detail)
  • two-sided (connected to both implementations and clients)
  • formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs)
  • live (connected via machine-checkable proofs to the implementation and client code).

We call these deep specifications.

The DeepSpec @ PLDI 2018 workshop aims to bring together researchers interested in Deep Specifications. Our goal is to promote the development of new science, technology, and tools–for specifying what programs should do, for building programs that conform to those specifications, and for verifying that programs do behave exactly as specified. This workshop will examine the role of verification in the context of core software-systems infrastructure such as operating systems, programming-language compilers, and computer chips; with applications such as elections and voting systems, cars, and smartphones.

More Information

The workshop program is still under construction!

This workshop is being held as part of the Science of Deep Specifications research project, which is funded by the National Science Foundation. For more information, see DeepSpec.org.

Workshop

Title

Five Minute Talks

DeepSpec @ PLDI 2018 will have a session devoted to five minute “lightning” talks. If you would like to participate, contact one of the workshop organizers (Steve Zdancewic or Stephanie Weirich) to submit a title and one-paragraph abstract. We will fill the available space on first-come/first-served basis.

Talks about all subjects of interest to the DeepSpec audience are welcome!

Mon 18 Jun

deepspec-2018-papers
09:00 - 10:30: DeepSpec 2018 - Deep Specifications at Columbus Ballroom B
deepspec-2018-papers09:00 - 10:00
Talk
Andrew AppelPrinceton
deepspec-2018-papers10:00 - 10:30
Talk
Magnus O. MyreenChalmers University of Technology, Sweden
deepspec-2018-papers
11:00 - 12:15: DeepSpec 2018 - LLVM at Columbus Ballroom B
deepspec-2018-papers11:00 - 11:30
Talk
Steve ZdancewicUniversity of Pennsylvania
deepspec-2018-papers11:30 - 12:00
Talk
Chung-Kil HurSeoul National University
deepspec-2018-papers
14:00 - 15:40: DeepSpec 2018 - From Testing to Verification at Columbus Ballroom B
deepspec-2018-papers14:00 - 14:30
Talk
deepspec-2018-papers14:30 - 15:00
Talk
Benjamin C. PierceUniversity of Pennsylvania
deepspec-2018-papers15:00 - 15:30
Talk
Leonidas LampropoulosUniversity of Pennsylvania
deepspec-2018-papers
16:10 - 17:35: DeepSpec 2018 - Hardware and Low-Level OS Verification at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:40
Talk
Zhong ShaoYale University
deepspec-2018-papers16:40 - 17:10
Talk
Adam ChlipalaMassachusetts Institute of Technology, USA
deepspec-2018-papers17:10 - 17:35
Talk

Tue 19 Jun

deepspec-2018-papers
09:00 - 10:30: DeepSpec 2018 - Distributed Systems and Cryptography at Columbus Ballroom B
deepspec-2018-papers09:00 - 10:00
Talk
Mooly SagivTel Aviv University
deepspec-2018-papers10:00 - 10:30
Talk
deepspec-2018-papers
11:00 - 12:15: DeepSpec 2018 - Haskell Core and Debugging Debuggers at Columbus Ballroom B
deepspec-2018-papers11:00 - 11:30
Talk
Stephanie WeirichUniversity of Pennsylvania, USA
deepspec-2018-papers11:30 - 12:00
Talk
deepspec-2018-papers
14:00 - 15:40: DeepSpec 2018 - Concurrency and Concurrent Operating Systems at Columbus Ballroom B
deepspec-2018-papers14:00 - 14:30
Talk
Jieung KimYale University, USA
deepspec-2018-papers14:30 - 15:00
Talk
Thomas SewellUNSW, Australia
deepspec-2018-papers15:00 - 15:30
Talk
William ManskyPrinceton University
deepspec-2018-papers
16:10 - 17:35: DeepSpec 2018 - Lightning Talks at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:15
Talk
deepspec-2018-papers16:15 - 16:20
Talk
deepspec-2018-papers16:20 - 16:25
Talk
Gordon StewartOhio University
deepspec-2018-papers16:25 - 16:30
Talk
deepspec-2018-papers16:30 - 16:35
Talk
deepspec-2018-papers16:35 - 16:40
Talk
deepspec-2018-papers16:40 - 16:45
Talk
Christine RizkallahUniversity of New South Wales
deepspec-2018-papers16:45 - 16:50
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA
deepspec-2018-papers16:50 - 16:55
Talk
Sam GruetterMassachusetts Institute of Technology