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

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

Sat 22 Jun
Times are displayed in time zone: Tijuana, Baja California change

08:00 - 09:00: BreakfastCatering at 301 Foyer
08:00 - 09:00
Other
Catering
09:00 - 10:30: Deep SpecificationsDeepSpec at 106B
Chair(s): Lennart BeringerPrinceton University
09:00 - 09:45
Talk
DeepSpec
Benjamin C. PierceUniversity of Pennsylvania
09:45 - 10:30
Talk
DeepSpec
Andrew AppelPrinceton, Adam ChlipalaMassachusetts Institute of Technology, USA, Zhong ShaoYale University
10:30 - 11:00: Coffee BreakDeepSpec at 106B
11:00 - 12:30: Compiler VerificationDeepSpec at 106B
Chair(s): Zhong ShaoYale University
11:00 - 11:30
Talk
DeepSpec
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
11:30 - 12:00
Talk
DeepSpec
Adam ChlipalaMassachusetts Institute of Technology, USA
12:00 - 12:30
Talk
DeepSpec
Yuting WangYale University
11:00 - 11:20: Coffee BreakCatering at 301 Foyer
11:00 - 11:20
Coffee break
Catering
12:30 - 14:00: LunchCatering at 301A
14:00 - 15:30: Modular ReasoningDeepSpec at 106B
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
14:00 - 14:30
Talk
DeepSpec
Lennart BeringerPrinceton University, Andrew AppelPrinceton
14:30 - 15:00
Talk
DeepSpec
Mengqi LiuYale University
15:00 - 15:30
Talk
DeepSpec
Joonwon ChoiMassachusetts Institute of Technology, USA
15:30 - 16:00: Coffee BreakCatering at 301 Foyer
16:00 - 17:30: Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew AppelPrinceton
16:00 - 16:20
Talk
DeepSpec
Steve ZdancewicUniversity of Pennsylvania
16:20 - 16:45
Talk
DeepSpec
William ManskyUniversity of Illinois at Chicago, Wolf Honore
16:45 - 17:30
Talk
DeepSpec
Daan LeijenMicrosoft Research, USA

Sun 23 Jun
Times are displayed in time zone: Tijuana, Baja California change

08:00 - 09:00: BreakfastCatering at 301 Foyer
09:00 - 10:30: Interaction Trees and Algebraic Effects IIDeepSpec at 106B
Chair(s): Steve ZdancewicUniversity of Pennsylvania
09:00 - 09:45
Talk
DeepSpec
Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
09:45 - 10:30
Talk
DeepSpec
James McKinnaUniversity of Edinburgh
10:30 - 11:00: Coffee BreakDeepSpec at 106B
11:00 - 12:30: HW/SW Interface SpecificationsDeepSpec at 106B
Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA
11:00 - 11:45
Talk
DeepSpec
11:45 - 12:30
Talk
DeepSpec
Yatin ManerkarPrinceton University
11:00 - 11:20: Coffee BreakCatering at 301 Foyer
12:30 - 14:00: LunchCatering at 301A
14:00 - 15:15: Verifying All the ThingsDeepSpec at 106B
Chair(s): Zhong ShaoYale University
14:00 - 14:45
Talk
DeepSpec
Ben LaurieGoogle Research
14:45 - 15:15
Talk
DeepSpec
Jérémie KoenigYale University
15:15 - 15:45: Coffee BreakDeepSpec at 106B
15:30 - 16:00: Coffee BreakCatering at 301 Foyer
15:45 - 16:45: Coinduction and TestingDeepSpec at 106B
Chair(s): Lennart BeringerPrinceton University
15:45 - 16:15
Talk
DeepSpec
Chung-Kil HurSeoul National University
16:15 - 16:45
Talk
DeepSpec
Leonidas LampropoulosUniversity of Pennsylvania