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

Title
Serializability for Distributed Protocols
DeepSpec
5-minute Lightning Talks
DeepSpec
A Formal Equational Theory for Call-By-Push-Value
DeepSpec
A Quick Hack to ask any SMT Solver if my Coq Goal is True
DeepSpec
Automation for High-Assurance Cryptography, for Primitives and Protocols
DeepSpec
CakeML: from functions to machine code with proof all the way
DeepSpec
Crellvm
DeepSpec
Debugging Debug Information and Beyond
DeepSpec
LLVM's IR and Call-By-Push-Value Lambda Calculus
DeepSpec
Machine-Verified Machine Learning
DeepSpec
Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems
DeepSpec
Multicore and Multithreaded Linking for Concurrent CertiKOS
DeepSpec
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
DeepSpec
Progress Report on the DeepSpec Web Server
DeepSpec
QuickChick: Random Testing in Coq
DeepSpec
Real-Time CertiKOS: A Step Toward Resource Adaptive Certified OS Kernels
DeepSpec
Simplicity for Smart Contracts
DeepSpec
Specifying and Verifying Concurrent Programs with Ghost State
DeepSpec
The Science of Deep Specification
DeepSpec
Towards a formal semantics for GHC Core
DeepSpec
Using Kami in the field - experiences integrating Kami into SiFive's Chisel/Scala-based design flow
DeepSpec
Vellvm - Modular Semantics via Interaction Trees
DeepSpec
Verifiable C, a logic and system for proving C programs correct
DeepSpec
Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels
DeepSpec
Verification of Union-Find in C
DeepSpec
Verifying seL4 towards Concurrency
DeepSpec

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!

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 18 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

09:00 - 10:30: Deep SpecificationsDeepSpec at Columbus Ballroom B
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 - 12:15: LLVMDeepSpec at Columbus Ballroom B
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 - 15:40: From Testing to VerificationDeepSpec at Columbus Ballroom B
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

Tue 19 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

11:00 - 12:15: Haskell Core and Debugging DebuggersDeepSpec at Columbus Ballroom B
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 - 15:40: Concurrency and Concurrent Operating SystemsDeepSpec at Columbus Ballroom B
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 - 17:35: Lightning TalksDeepSpec at Columbus Ballroom B
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
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