Tue 19 Jun 2018 16:25 - 16:30 at Columbus Ballroom B - Lightning Talks
We developed a general framework of graph theory which is powerful enough to support realistic verification. The work is built on CompCert—a verified compiler, and VST—a series of machine-checked modules focusing on reasoning programs that can be compiled with the CompCert compiler. With the framework we finished end-to-end, full functional correctness verification for several classical graph-manipulating algorithms: graph mark, spanning tree, union-find, etc. I’ll illustrate the verification of union-find in the talk.
Tue 19 JunDisplayed time zone: Eastern Time (US & Canada) change
Tue 19 Jun
Displayed time zone: Eastern Time (US & Canada) change
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 | ||
