DeepSpec 2018

About
Program

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 Joonwon Choi
	5-minute Lightning Talks
	A Formal Equational Theory for Call-By-Push-Value Christine Rizkallah
	A Quick Hack to ask any SMT Solver if my Coq Goal is True Sam Gruetter
	Automation for High-Assurance Cryptography, for Primitives and Protocols Andres Erbsen
	CakeML: from functions to machine code with proof all the way Magnus O. Myreen
	Crellvm Chung-Kil Hur
	Debugging Debug Information and Beyond Francesco Zappa Nardelli
	LLVM's IR and Call-By-Push-Value Lambda Calculus Yannick Zakowski
	Machine-Verified Machine Learning Gordon Stewart
	Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems Mooly Sagiv
	Multicore and Multithreaded Linking for Concurrent CertiKOS Jieung Kim
	Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats Clément Pit-Claudel
	Progress Report on the DeepSpec Web Server Benjamin C. Pierce
	QuickChick: Random Testing in Coq Leonidas Lampropoulos
	Real-Time CertiKOS: A Step Toward Resource Adaptive Certified OS Kernels Zhong Shao
	Simplicity for Smart Contracts Russell O'Connor
	Specifying and Verifying Concurrent Programs with Ghost State William Mansky
	The Science of Deep Specification Andrew Appel
	Towards a formal semantics for GHC Core Stephanie Weirich
	Using Kami in the field - experiences integrating Kami into SiFive's Chisel/Scala-based design flow Muralidaran Vijayaraghavan
	Vellvm - Modular Semantics via Interaction Trees Steve Zdancewic
	Verifiable C, a logic and system for proving C programs correct Qinxiang Cao
	Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels Adam Chlipala
	Verification of Union-Find in C Shengyi Wang
	Verifying seL4 towards Concurrency Thomas Sewell

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!