Deep Specifications
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 2018 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
The workshop program is still under construction!
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
Five Minute Talks
DeepSpec @ PLDI 2018 will have a session devoted to five minute “lightning” talks. If you would like to participate, contact one of the workshop organizers (Steve Zdancewic or Stephanie Weirich) to submit a title and one-paragraph abstract. We will fill the available space on first-come/first-served basis.
Talks about all subjects of interest to the DeepSpec audience are welcome!
Mon 18 Jun Times are displayed in time zone: Eastern Time (US & Canada) change
| 09:00 - 10:00 Talk | The Science of Deep Specification DeepSpec Andrew AppelPrinceton | ||
| 10:00 - 10:30 Talk | CakeML: from functions to machine code with proof all the way DeepSpec Magnus O. MyreenChalmers University of Technology, Sweden | ||
| 11:00 - 11:30 Talk | Vellvm - Modular Semantics via Interaction Trees DeepSpec Steve ZdancewicUniversity of Pennsylvania | ||
| 11:30 - 12:00 Talk | Crellvm DeepSpec Chung-Kil HurSeoul National University | ||
| 14:00 - 14:30 Talk | Verifiable C, a logic and system for proving C programs correct DeepSpec | ||
| 14:30 - 15:00 Talk | Progress Report on the DeepSpec Web Server DeepSpec Benjamin C. PierceUniversity of Pennsylvania | ||
| 15:00 - 15:30 Talk | QuickChick: Random Testing in Coq DeepSpec Leonidas LampropoulosUniversity of Pennsylvania | ||
| 16:10 - 16:40 Talk | Real-Time CertiKOS: A Step Toward Resource Adaptive Certified OS Kernels DeepSpec Zhong ShaoYale University | ||
| 16:40 - 17:10 Talk | Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels DeepSpec Adam ChlipalaMassachusetts Institute of Technology, USA | ||
| 17:10 - 17:35 Talk | Using Kami in the field - experiences integrating Kami into SiFive's Chisel/Scala-based design flow DeepSpec | ||
Tue 19 Jun Times are displayed in time zone: Eastern Time (US & Canada) change
| 09:00 - 10:00 Talk | Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems DeepSpec Mooly SagivTel Aviv University | ||
| 10:00 - 10:30 Talk | Automation for High-Assurance Cryptography, for Primitives and Protocols DeepSpec | ||
| 11:00 - 11:30 Talk | Towards a formal semantics for GHC Core DeepSpec Stephanie WeirichUniversity of Pennsylvania, USA | ||
| 11:30 - 12:00 Talk | Debugging Debug Information and Beyond DeepSpec | ||
| 14:00 - 14:30 Talk | Multicore and Multithreaded Linking for Concurrent CertiKOS DeepSpec Jieung KimYale University, USA | ||
| 14:30 - 15:00 Talk | Verifying seL4 towards Concurrency DeepSpec Thomas SewellUNSW, Australia | ||
| 15:00 - 15:30 Talk | Specifying and Verifying Concurrent Programs with Ghost State DeepSpec William ManskyPrinceton University | ||
| 16:10 - 16:15 Talk | 5-minute Lightning Talks DeepSpec | ||
| 16:15 - 16:20 Talk | Simplicity for Smart Contracts DeepSpec | ||
| 16:20 - 16:25 Talk | Machine-Verified Machine Learning DeepSpec Gordon StewartOhio University | ||
| 16:25 - 16:30 Talk | Verification of Union-Find in C DeepSpec | ||
| 16:30 - 16:35 Talk | Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats DeepSpec Clément Pit-ClaudelMIT CSAIL | ||
| 16:35 - 16:40 Talk | LLVM's IR and Call-By-Push-Value Lambda Calculus DeepSpec | ||
| 16:40 - 16:45 Talk | A Formal Equational Theory for Call-By-Push-Value DeepSpec Christine RizkallahUniversity of New South Wales | ||
| 16:45 - 16:50 Talk | Serializability for Distributed Protocols DeepSpec Joonwon ChoiMassachusetts Institute of Technology, USA | ||
| 16:50 - 16:55 Talk | A Quick Hack to ask any SMT Solver if my Coq Goal is True DeepSpec Sam GruetterMassachusetts Institute of Technology | ||
