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
Sat 22 JunDisplayed time zone: Tijuana, Baja California change
09:00 - 10:30 | |||
09:00 45mTalk | Overview of the DeepSpec Expedition and its Capstone Application DeepSpec Benjamin C. Pierce University of Pennsylvania | ||
09:45 45mTalk | Project Updates from Participating Sites DeepSpec Andrew W. Appel Princeton, Adam Chlipala Massachusetts Institute of Technology, USA, Zhong Shao Yale University | ||
11:00 - 12:30 | |||
11:00 30mTalk | Closure Conversion is Safe for Space DeepSpec | ||
11:30 30mTalk | Fast, Verified Partial Evaluation DeepSpec Adam Chlipala Massachusetts Institute of Technology, USA | ||
12:00 30mTalk | Stack-Aware CompCert DeepSpec Yuting Wang Yale University | ||
14:00 - 15:30 | |||
14:00 30mTalk | Abstraction, Subsumption, and Linking in VST DeepSpec | ||
14:30 30mTalk | Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation DeepSpec Mengqi Liu Yale University | ||
15:00 30mTalk | Modular Correctness Proofs at the Hardware-Software Interface DeepSpec Joonwon Choi Massachusetts Institute of Technology, USA | ||
16:00 - 17:30 | |||
16:00 20mTalk | Interaction Trees: Representing Recursive and Impure Programs in Coq DeepSpec Steve Zdancewic University of Pennsylvania | ||
16:20 25mTalk | Connecting Separation Logic with First-Order Reasoning on Memory DeepSpec | ||
16:45 45mTalk | Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control) DeepSpec Daan Leijen Microsoft Research, USA | ||
Sun 23 JunDisplayed time zone: Tijuana, Baja California change
09:00 - 10:30 | Interaction Trees and Algebraic Effects IIDeepSpec at 106B Chair(s): Steve Zdancewic University of Pennsylvania | ||
09:00 45mTalk | 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 45mTalk | Names, Places, and Things: Generic Traversals over Generic Syntax with Binding DeepSpec James McKinna University of Edinburgh | ||
11:00 - 12:30 | HW/SW Interface SpecificationsDeepSpec at 106B Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA | ||
11:00 45mTalk | Development of the RISC-V ISA Formal Specification DeepSpec | ||
11:45 45mTalk | Automated Formal Memory Consistency Verification of Hardware DeepSpec Yatin Manerkar Princeton University | ||
14:00 - 15:15 | |||
14:00 45mTalk | Project Oak: Control Data in Distributed Systems, Verify All The Things DeepSpec Ben Laurie Google Research | ||
14:45 30mTalk | Refinement-Based Game Semantics for CompCert DeepSpec Jérémie Koenig Yale University | ||
15:45 - 16:45 | |||
15:45 30mTalk | Coinductive Reasoning about Interaction Trees DeepSpec Chung-Kil Hur Seoul National University | ||
16:15 30mTalk | Coverage Guided, Property Based Testing DeepSpec Leonidas Lampropoulos University of Pennsylvania | ||
