DPA 2019
Sat 22 - Wed 26 June 2019 Phoenix, Arizona, United States
co-located with PLDI 2019
VenuePhoenix Convention Center
Room name106B
Floor0
Room number106B
Room InformationNo extra information available
Program

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

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

09:00 - 10:30
Deep SpecificationsDeepSpec at 106B
Chair(s): Lennart Beringer Princeton University
09:00
45m
Talk
Overview of the DeepSpec Expedition and its Capstone Application
DeepSpec
Benjamin C. Pierce University of Pennsylvania
09:45
45m
Talk
Project Updates from Participating Sites
DeepSpec
Andrew W. Appel Princeton, Adam Chlipala Massachusetts Institute of Technology, USA, Zhong Shao Yale University
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
Compiler VerificationDeepSpec at 106B
Chair(s): Zhong Shao Yale University
11:00
30m
Talk
Closure Conversion is Safe for Space
DeepSpec
Zoe Paraskevopoulou Princeton University, Andrew W. Appel Princeton
11:30
30m
Talk
Fast, Verified Partial Evaluation
DeepSpec
Adam Chlipala Massachusetts Institute of Technology, USA
12:00
30m
Talk
Stack-Aware CompCert
DeepSpec
Yuting Wang Yale University
14:00 - 15:30
Modular ReasoningDeepSpec at 106B
Chair(s): Benjamin C. Pierce University of Pennsylvania
14:00
30m
Talk
Abstraction, Subsumption, and Linking in VST
DeepSpec
Lennart Beringer Princeton University, Andrew W. Appel Princeton
14:30
30m
Talk
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Mengqi Liu Yale University
15:00
30m
Talk
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Joonwon Choi Massachusetts Institute of Technology, USA
16:00 - 17:30
Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew W. Appel Princeton
16:00
20m
Talk
Interaction Trees: Representing Recursive and Impure Programs in Coq
DeepSpec
Steve Zdancewic University of Pennsylvania
16:20
25m
Talk
Connecting Separation Logic with First-Order Reasoning on Memory
DeepSpec
William Mansky University of Illinois at Chicago, Wolf Honore
16:45
45m
Talk
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
DeepSpec
Daan Leijen Microsoft Research, USA

Sun 23 Jun

Displayed time zone: Tijuana, Baja California change

09:00 - 10:30
Interaction Trees and Algebraic Effects IIDeepSpec at 106B
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
45m
Talk
Implementation and Verification of Modular Effectful Systems in Coq using FreeSpec
DeepSpec
Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
09:45
45m
Talk
Names, Places, and Things: Generic Traversals over Generic Syntax with Binding
DeepSpec
James McKinna University of Edinburgh
10:30 - 11:00
Coffee BreakDeepSpec at 106B
11:00 - 12:30
HW/SW Interface SpecificationsDeepSpec at 106B
Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA
11:00
45m
Talk
Development of the RISC-V ISA Formal Specification
DeepSpec
11:45
45m
Talk
Automated Formal Memory Consistency Verification of Hardware
DeepSpec
Yatin Manerkar Princeton University
14:00 - 15:15
Verifying All the ThingsDeepSpec at 106B
Chair(s): Zhong Shao Yale University
14:00
45m
Talk
Project Oak: Control Data in Distributed Systems, Verify All The Things
DeepSpec
Ben Laurie Google Research
14:45
30m
Talk
Refinement-Based Game Semantics for CompCert
DeepSpec
Jérémie Koenig Yale University
15:15 - 15:45
Coffee BreakDeepSpec at 106B
15:45 - 16:45
Coinduction and TestingDeepSpec at 106B
Chair(s): Lennart Beringer Princeton University
15:45
30m
Talk
Coinductive Reasoning about Interaction Trees
DeepSpec
Chung-Kil Hur Seoul National University
16:15
30m
Talk
Coverage Guided, Property Based Testing
DeepSpec
Leonidas Lampropoulos University of Pennsylvania