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
Abstraction, Subsumption, and Linking in VST
DeepSpec
Automated Formal Memory Consistency Verification of Hardware
DeepSpec
Closure Conversion is Safe for Space
DeepSpec
Coinductive Reasoning about Interaction Trees
DeepSpec
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
Coverage Guided, Property Based Testing
DeepSpec
Development of the RISC-V ISA Formal Specification
DeepSpec
Fast, Verified Partial Evaluation
DeepSpec
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
DeepSpec
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
DeepSpec
Overview of the DeepSpec Expedition and its Capstone Application
DeepSpec
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec
Project Updates from Participating Sites
DeepSpec
Refinement-Based Game Semantics for CompCert
DeepSpec
Stack-Aware CompCert
DeepSpec
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Dates
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

08:00 - 09:00
BreakfastCatering at 301 Foyer
08:00
60m
Other
Breakfast
Catering

09:00 - 10:30
Deep SpecificationsDeepSpec at 106B
Chair(s): Lennart Beringer Princeton University
09:00
45m
Talk
Overview of the DeepSpec Expedition and its Capstone Application
DeepSpec
Benjamin C. Pierce University of Pennsylvania
09:45
45m
Talk
Project Updates from Participating Sites
DeepSpec
Andrew W. Appel Princeton, Adam Chlipala Massachusetts Institute of Technology, USA, Zhong Shao Yale University
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
Compiler VerificationDeepSpec at 106B
Chair(s): Zhong Shao Yale University
11:00
30m
Talk
Closure Conversion is Safe for Space
DeepSpec
Zoe Paraskevopoulou Princeton University, Andrew W. Appel Princeton
11:30
30m
Talk
Fast, Verified Partial Evaluation
DeepSpec
Adam Chlipala Massachusetts Institute of Technology, USA
12:00
30m
Talk
Stack-Aware CompCert
DeepSpec
Yuting Wang Yale University
11:00 - 11:20
Coffee BreakCatering at 301 Foyer
11:00
20m
Coffee break
Break
Catering

12:30 - 14:00
LunchCatering at 301A
14:00 - 15:30
Modular ReasoningDeepSpec at 106B
Chair(s): Benjamin C. Pierce University of Pennsylvania
14:00
30m
Talk
Abstraction, Subsumption, and Linking in VST
DeepSpec
Lennart Beringer Princeton University, Andrew W. Appel Princeton
14:30
30m
Talk
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Mengqi Liu Yale University
15:00
30m
Talk
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Joonwon Choi Massachusetts Institute of Technology, USA
15:30 - 16:00
Coffee BreakCatering at 301 Foyer
16:00 - 17:30
Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew W. Appel Princeton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve Zdancewic University of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William Mansky University of Illinois at Chicago, Wolf Honore
16:45
45m
Talk
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Daan Leijen Microsoft Research, USA

Sun 23 Jun

Displayed time zone: Tijuana, Baja California change

08:00 - 09:00
BreakfastCatering at 301 Foyer
09:00 - 10:30
Interaction Trees and Algebraic Effects IIDeepSpec at 106B
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
45m
Talk
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
DeepSpec
Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
09:45
45m
Talk
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
DeepSpec
James McKinna University of Edinburgh
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
HW/SW Interface SpecificationsDeepSpec at 106B
Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA
11:00
45m
Talk
Development of the RISC-V ISA Formal Specification
DeepSpec
11:45
45m
Talk
Automated Formal Memory Consistency Verification of Hardware
DeepSpec
Yatin Manerkar Princeton University
11:00 - 11:20
Coffee BreakCatering at 301 Foyer
12:30 - 14:00
LunchCatering at 301A
14:00 - 15:15
Verifying All the ThingsDeepSpec at 106B
Chair(s): Zhong Shao Yale University
14:00
45m
Talk
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec
Ben Laurie Google Research
14:45
30m
Talk
Refinement-Based Game Semantics for CompCert
DeepSpec
Jérémie Koenig Yale University
15:15 - 15:45
Coffee BreakDeepSpec at 106B
15:30 - 16:00
Coffee BreakCatering at 301 Foyer
15:45 - 16:45
Coinduction and TestingDeepSpec at 106B
Chair(s): Lennart Beringer Princeton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil Hur Seoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas Lampropoulos University of Pennsylvania