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 Jun Times are displayed in 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. PierceUniversity of Pennsylvania | ||
09:45 45mTalk | Project Updates from Participating Sites DeepSpec Andrew AppelPrinceton, Adam ChlipalaMassachusetts Institute of Technology, USA, Zhong ShaoYale University | ||
11:00 - 12:30 | |||
11:00 30mTalk | Closure Conversion is Safe for Space DeepSpec | ||
11:30 30mTalk | Fast, Verified Partial Evaluation DeepSpec Adam ChlipalaMassachusetts Institute of Technology, USA | ||
12:00 30mTalk | Stack-Aware CompCert DeepSpec Yuting WangYale 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 LiuYale University | ||
15:00 30mTalk | Modular Correctness Proofs at the Hardware-Software Interface DeepSpec Joonwon ChoiMassachusetts Institute of Technology, USA | ||
16:00 - 17:30 | |||
16:00 20mTalk | Interaction Trees: Representing Recursive and Impure Programs in Coq DeepSpec Steve ZdancewicUniversity 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 LeijenMicrosoft Research, USA | ||
Sun 23 Jun Times are displayed in time zone: Tijuana, Baja California change
09:00 - 10:30 | Interaction Trees and Algebraic Effects IIDeepSpec at 106B Chair(s): Steve ZdancewicUniversity of Pennsylvania | ||
09:00 45mTalk | 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 45mTalk | Names, Places, and Things: Generic Traversals over Generic Syntax with Binding DeepSpec James McKinnaUniversity of Edinburgh | ||
11:00 - 12:30 | HW/SW Interface SpecificationsDeepSpec at 106B Chair(s): Adam ChlipalaMassachusetts 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 ManerkarPrinceton University | ||
14:00 - 15:15 | |||
14:00 45mTalk | Project Oak: Control Data in Distributed Systems, Verify All The Things DeepSpec Ben LaurieGoogle Research | ||
14:45 30mTalk | Refinement-Based Game Semantics for CompCert DeepSpec Jérémie KoenigYale University | ||
15:45 - 16:45 | |||
15:45 30mTalk | Coinductive Reasoning about Interaction Trees DeepSpec Chung-Kil HurSeoul National University | ||
16:15 30mTalk | Coverage Guided, Property Based Testing DeepSpec Leonidas LampropoulosUniversity of Pennsylvania | ||
