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

Displayed time zone: Eastern Time (US & Canada) change