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

Conference Day
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 BeringerPrinceton University
09:00
45m
Talk
Overview of the DeepSpec Expedition and its Capstone Application
DeepSpec
Benjamin C. PierceUniversity of Pennsylvania
09:45
45m
Talk
Project Updates from Participating Sites
DeepSpec
Andrew AppelPrinceton, Adam ChlipalaMassachusetts Institute of Technology, USA, Zhong ShaoYale University
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
Compiler VerificationDeepSpec at 106B
Chair(s): Zhong ShaoYale University
11:00
30m
Talk
Closure Conversion is Safe for Space
DeepSpec
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
11:30
30m
Talk
Fast, Verified Partial Evaluation
DeepSpec
Adam ChlipalaMassachusetts Institute of Technology, USA
12:00
30m
Talk
Stack-Aware CompCert
DeepSpec
Yuting WangYale 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. PierceUniversity of Pennsylvania
14:00
30m
Talk
Abstraction, Subsumption, and Linking in VST
DeepSpec
Lennart BeringerPrinceton University, Andrew AppelPrinceton
14:30
30m
Talk
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Mengqi LiuYale University
15:00
30m
Talk
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Joonwon ChoiMassachusetts 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 AppelPrinceton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve ZdancewicUniversity of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William ManskyUniversity 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 LeijenMicrosoft Research, USA

Conference Day
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 ZdancewicUniversity of Pennsylvania
09:00
45m
Talk
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
DeepSpec
Yann Régis-GianasIRIF, 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 McKinnaUniversity of Edinburgh
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
HW/SW Interface SpecificationsDeepSpec at 106B
Chair(s): Adam ChlipalaMassachusetts 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 ManerkarPrinceton 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 ShaoYale University
14:00
45m
Talk
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec
Ben LaurieGoogle Research
14:45
30m
Talk
Refinement-Based Game Semantics for CompCert
DeepSpec
Jérémie KoenigYale 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 BeringerPrinceton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil HurSeoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas LampropoulosUniversity of Pennsylvania