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
No schedule yet

Not scheduled yet

deepspec-2018-papersNot scheduled yet
Talk
Andrew Appel
deepspec-2018-papersNot scheduled yet
Talk
Qinxiang Cao
deepspec-2018-papersNot scheduled yet
Talk
Mooly Sagiv
deepspec-2018-papersNot scheduled yet
Talk
Steve Zdancewic
deepspec-2018-papersNot scheduled yet
Talk
Magnus O. Myreen
deepspec-2018-papersNot scheduled yet
Talk
Chung-Kil Hur
deepspec-2018-papersNot scheduled yet
Talk
Stephanie Weirich