Verifying Imperative Programs using Auto2

Title:	Verifying Imperative Programs using Auto2
Author:	Bohua Zhan
Submission date:	2018-12-21
Abstract:	This entry contains the application of auto2 to verifying functional and imperative programs. Algorithms and data structures that are verified include linked lists, binary search trees, red-black trees, interval trees, priority queue, quicksort, union-find, Dijkstra's algorithm, and a sweep-line algorithm for detecting rectangle intersection. The imperative verification is based on Imperative HOL and its separation logic framework. A major goal of this work is to set up automation in order to reduce the length of proof that the user needs to provide, both for verifying functional programs and for working with separation logic.
BibTeX:	@article{Auto2_Imperative_HOL-AFP, author = {Bohua Zhan}, title = {Verifying Imperative Programs using Auto2}, journal = {Archive of Formal Proofs}, month = dec, year = 2018, note = {\url{http://isa-afp.org/entries/Auto2_Imperative_HOL.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Auto2_HOL
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.