DOCTORAL SEMINAR

Mechanized Verification of Graph-manipulating Programs

Speaker
Mr Wang Shengyi
Advisor
Dr Aquinas Adam Hobor, Assistant Professor, School of Computing


27 Sep 2018 Thursday, 04:30 PM to 06:00 PM

Executive Classroom, COM2-04-02

Abstract:

Over the last fifteen years great strides have been made in automating verifications of programs that manipulate tree-like data structures using separation logic. Unfortunately, verifying programs that manipulate graph-like data structures (i.e. structures with intrinsic sharing) has been more challenging, especially for modular reasoning.

In thesis we explore and develop a general and more simple way to verify realistic graph-manipulating programs mechanically. This verification focuses on proving the fully functional correctness of graph algorithms formally and manually. We intend to verify real, runnable programs written in C programming language.

We propose a general and modular framework for graph-related reasoning which can be roughly split into two parts: a formalization of graph theory in mathematics and a spatial library in separation logic. The latter connects the underlying mathematical graph model and the graph representations in heaps. Our framework is expressive and powerful enough to adapt various requirements of graphs in different applications. We use the framework to verify several graph-manipulating algorithms, including graph mark, spanning tree and two versions of union-find.