Mechanized Verification of Graph-manipulating Programs
王盛颐，National University of Singapore
2019-10-09 13:30:00 ~ 2019-10-09 15:00:00
Room 1319, Software Expert Building
Qinxiang Cao, Assistant Professor, John Hopcroft Center for Computer Science
We develop powerful and general techniques to mechanically verify realistic programs that manipulate heap-represented graphs. These graphs can exhibit well-known organization principles, such as being a directed acyclic graph or a disjoint-forest; alternatively, these graphs can be totally unstructured. The common thread for such structures is that they exhibit deep intrinsic sharing and can be expressed using the language of graph theory. We construct a modular and general setup for reasoning about abstract mathematical graphs and use separation logic to define how such abstract graphs are represented concretely in the heap. We develop a Localize rule that enables modular reasoning about such programs, and show how this rule can support existential quantifiers in postconditions and smoothly handle modified program variables. We demonstrate the generality and power of our techniques by integrating them into the Verified Software Toolchain and certifying the correctness of seven graph-manipulating programs written in CompCert C, including a 400-line generational garbage collector for the CertiCoq project.
Shengyi Wang is a PhD candidate from School of Computing, National University of Singapore. He received the M.S. in applied mathematics and B.S. in mathematics from Peking University. He is interested in the formalization of mathematical structures and improving software quality through formal verification.