### 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.

### License

BSD License

### Topics

- Computer science/Algorithms
- Computer science/Data structures

### Session Auto2_Imperative_HOL

- Mapping_Str
- Lists_Ex
- BST
- Partial_Equiv_Rel
- Union_Find
- Connectivity
- Arrays_Ex
- Dijkstra
- Interval
- Interval_Tree
- Quicksort
- Indexed_PQueue
- RBTree
- Rect_Intersect
- SepLogic_Base
- SepAuto
- GCD_Impl
- LinkedList
- BST_Impl
- RBTree_Impl
- Arrays_Impl
- Quicksort_Impl
- Union_Find_Impl
- Connectivity_Impl
- DynamicArray
- Indexed_PQueue_Impl
- Dijkstra_Impl
- IntervalTree_Impl
- Rect_Intersect_Impl
- Sep_Examples

### Depends on

- Auto2 Prover

### Auto-related entries

- Combinatorial Enumeration Algorithms
- Unbounded Separation Logic
- Skip Lists
- Hoare Logics for Time Bounds
- Treaps

## Cite

×

Auto2_Imperative_HOL-AFP

    @article{Auto2_Imperative_HOL-AFP,
      author  = {Bohua Zhan},
      title   = {Verifying Imperative Programs using Auto2},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Auto2_Imperative_HOL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Jan 22, 2019 : Isabelle2018