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 Jun

deepspec-2018-papers
16:10 - 17:35: DeepSpec 2018 - Lightning Talks at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:15
Talk
deepspec-2018-papers16:15 - 16:20
Talk
deepspec-2018-papers16:20 - 16:25
Talk
Gordon StewartOhio University
deepspec-2018-papers16:25 - 16:30
Talk
deepspec-2018-papers16:30 - 16:35
Talk
deepspec-2018-papers16:35 - 16:40
Talk
deepspec-2018-papers16:40 - 16:45
Talk
Christine RizkallahUniversity of New South Wales
deepspec-2018-papers16:45 - 16:50
Talk
Joonwon ChoiMassachusetts Institute of Technology, USA
deepspec-2018-papers16:50 - 16:55
Talk
Sam GruetterMassachusetts Institute of Technology