PLDI 2018 (series) / DeepSpec 2018 (series) /
DeepSpec 2018 Program
This is the DeepSpec 2018 program - see the full program for PLDI 2018 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 18 JunDisplayed time zone: Eastern Time (US & Canada) change
Mon 18 Jun
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mTalk | The Science of Deep Specification DeepSpec Andrew W. Appel Princeton | ||
10:00 30mTalk | CakeML: from functions to machine code with proof all the way DeepSpec Magnus O. Myreen Chalmers University of Technology, Sweden |
11:00 - 12:15 | |||
11:00 30mTalk | Vellvm - Modular Semantics via Interaction Trees DeepSpec Steve Zdancewic University of Pennsylvania | ||
11:30 30mTalk | Crellvm DeepSpec Chung-Kil Hur Seoul National University |
14:00 - 15:40 | |||
14:00 30mTalk | Verifiable C, a logic and system for proving C programs correct DeepSpec | ||
14:30 30mTalk | Progress Report on the DeepSpec Web Server DeepSpec Benjamin C. Pierce University of Pennsylvania | ||
15:00 30mTalk | QuickChick: Random Testing in Coq DeepSpec Leonidas Lampropoulos University of Pennsylvania |
16:10 - 17:35 | |||
16:10 30mTalk | Real-Time CertiKOS: A Step Toward Resource Adaptive Certified OS Kernels DeepSpec Zhong Shao Yale University | ||
16:40 30mTalk | Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels DeepSpec Adam Chlipala Massachusetts Institute of Technology, USA | ||
17:10 25mTalk | Using Kami in the field - experiences integrating Kami into SiFive's Chisel/Scala-based design flow DeepSpec Muralidaran Vijayaraghavan SiFive |
Tue 19 JunDisplayed time zone: Eastern Time (US & Canada) change
Tue 19 Jun
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mTalk | Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems DeepSpec Mooly Sagiv Tel Aviv University | ||
10:00 30mTalk | Automation for High-Assurance Cryptography, for Primitives and Protocols DeepSpec |
11:00 - 12:15 | |||
11:00 30mTalk | Towards a formal semantics for GHC Core DeepSpec Stephanie Weirich University of Pennsylvania, USA | ||
11:30 30mTalk | Debugging Debug Information and Beyond DeepSpec Francesco Zappa Nardelli Inria |
14:00 - 15:40 | |||
14:00 30mTalk | Multicore and Multithreaded Linking for Concurrent CertiKOS DeepSpec Jieung Kim Yale University, USA | ||
14:30 30mTalk | Verifying seL4 towards Concurrency DeepSpec Thomas Sewell UNSW, Australia | ||
15:00 30mTalk | Specifying and Verifying Concurrent Programs with Ghost State DeepSpec William Mansky Princeton University |
16:10 - 17:35 | |||
16:10 5mTalk | 5-minute Lightning Talks DeepSpec | ||
16:15 5mTalk | Simplicity for Smart Contracts DeepSpec | ||
16:20 5mTalk | Machine-Verified Machine Learning DeepSpec Gordon Stewart Ohio University | ||
16:25 5mTalk | Verification of Union-Find in C DeepSpec | ||
16:30 5mTalk | Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats DeepSpec Clément Pit-Claudel MIT CSAIL | ||
16:35 5mTalk | LLVM's IR and Call-By-Push-Value Lambda Calculus DeepSpec | ||
16:40 5mTalk | A Formal Equational Theory for Call-By-Push-Value DeepSpec Christine Rizkallah The University of Melbourne | ||
16:45 5mTalk | Serializability for Distributed Protocols DeepSpec Joonwon Choi Massachusetts Institute of Technology, USA | ||
16:50 5mTalk | A Quick Hack to ask any SMT Solver if my Coq Goal is True DeepSpec Samuel Gruetter Massachusetts Institute of Technology |