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

### Topics

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