
Verifying
Imperative
Programs
using
Auto2
Title: 
Verifying Imperative Programs using Auto2 
Author:

Bohua Zhan

Submission date: 
20181221 
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, redblack trees,
interval trees, priority queue, quicksort, unionfind, Dijkstra's
algorithm, and a sweepline 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_HOLAFP,
author = {Bohua Zhan},
title = {Verifying Imperative Programs using Auto2},
journal = {Archive of Formal Proofs},
month = dec,
year = 2018,
note = {\url{http://isaafp.org/entries/Auto2_Imperative_HOL.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Auto2_HOL 
