|
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{https://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.
|
|