Deep Specifications

The workshop will be held on June 22-23 (Saturday and Sunday).

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 2019 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

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
Dates

Sat 22 Jun

pldi-2019-catering
08:00 - 09:00: Catering - Breakfast at 301 Foyer
pldi-2019-catering08:00 - 09:00
Other
deepspec-2019-papers
09:00 - 10:30: DeepSpec 2019 - Deep Specifications at 106B
Chair(s): Lennart BeringerPrinceton University
deepspec-2019-papers09:00 - 09:45
Talk
Benjamin C. PierceUniversity of Pennsylvania
deepspec-2019-papers09:45 - 10:30
Talk
Andrew AppelPrinceton, Adam ChlipalaMassachusetts Institute of Technology, USA, Zhong ShaoYale University
deepspec-2019-papers
10:30 - 11:00: DeepSpec 2019 - Coffee Break at 106B
pldi-2019-catering
11:00 - 11:20: Catering - Coffee Break at 301 Foyer
pldi-2019-catering11:00 - 11:20
Coffee break
deepspec-2019-papers
11:00 - 12:30: DeepSpec 2019 - Compiler Verification at 106B
Chair(s): Zhong ShaoYale University
deepspec-2019-papers11:00 - 11:30
Talk
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
deepspec-2019-papers11:30 - 12:00
Talk
Adam ChlipalaMassachusetts Institute of Technology, USA
deepspec-2019-papers12:00 - 12:30
Talk
Yuting WangYale University
pldi-2019-catering
12:30 - 14:00: Catering - Lunch at 301A
deepspec-2019-papers
14:00 - 15:30: DeepSpec 2019 - Modular Reasoning at 106B
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
deepspec-2019-papers14:00 - 14:30
Talk
Lennart BeringerPrinceton University, Andrew AppelPrinceton
deepspec-2019-papers14:30 - 15:00
Talk
Mengqi LiuYale University
deepspec-2019-papers15:00 - 15:30
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA
pldi-2019-catering
15:30 - 16:00: Catering - Coffee Break at 301 Foyer
deepspec-2019-papers
16:00 - 17:30: DeepSpec 2019 - Interaction Trees and Algebraic Effects I at 106B
Chair(s): Andrew AppelPrinceton
deepspec-2019-papers16:00 - 16:20
Talk
Steve ZdancewicUniversity of Pennsylvania
deepspec-2019-papers16:20 - 16:45
Talk
William ManskyUniversity of Illinois at Chicago, Wolf Honore
deepspec-2019-papers16:45 - 17:30
Talk
Daan LeijenMicrosoft Research, USA

Sun 23 Jun

pldi-2019-catering
08:00 - 09:00: Catering - Breakfast at 301 Foyer
deepspec-2019-papers
09:00 - 10:30: DeepSpec 2019 - Interaction Trees and Algebraic Effects II at 106B
Chair(s): Steve ZdancewicUniversity of Pennsylvania
deepspec-2019-papers09:00 - 09:45
Talk
Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
deepspec-2019-papers09:45 - 10:30
Talk
James McKinnaUniversity of Edinburgh
deepspec-2019-papers
10:30 - 11:00: DeepSpec 2019 - Coffee Break at 106B
pldi-2019-catering
11:00 - 11:20: Catering - Coffee Break at 301 Foyer
deepspec-2019-papers
11:00 - 12:30: DeepSpec 2019 - HW/SW Interface Specifications at 106B
Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA
deepspec-2019-papers11:00 - 11:45
Talk
deepspec-2019-papers11:45 - 12:30
Talk
Yatin ManerkarPrinceton University
pldi-2019-catering
12:30 - 14:00: Catering - Lunch at 301A
deepspec-2019-papers
14:00 - 15:15: DeepSpec 2019 - Verifying All the Things at 106B
Chair(s): Zhong ShaoYale University
deepspec-2019-papers14:00 - 14:45
Talk
Ben LaurieGoogle Research
deepspec-2019-papers14:45 - 15:15
Talk
Jérémie KoenigYale University
deepspec-2019-papers
15:15 - 15:45: DeepSpec 2019 - Coffee Break at 106B
pldi-2019-catering
15:30 - 16:00: Catering - Coffee Break at 301 Foyer
deepspec-2019-papers
15:45 - 16:45: DeepSpec 2019 - Coinduction and Testing at 106B
Chair(s): Lennart BeringerPrinceton University
deepspec-2019-papers15:45 - 16:15
Talk
Chung-Kil HurSeoul National University
deepspec-2019-papers16:15 - 16:45
Talk
Leonidas LampropoulosUniversity of Pennsylvania