Efficient Verification of Imperative Programs Using Auto2
Abstract
Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the setup of auto2 for both stages of the proof process: verification of a functional version of the program, and refining to the imperative version using separation logic. As examples, we verify several data structures, including redblack trees, interval trees, priority queues, and unionfind. We also verify several algorithms making use of these data structures. These examples show that our framework is able to verify complex algorithms efficiently and in a modular manner.
1 Introduction
Verification of imperative programs has been a wellstudied area. While work on separation logic addressed the main theoretical issues, verification in practice is still a tedious process. Even if we limit to the case of sequential programs with relatively simple memoryallocation patterns, verification is still difficult when a lot of mathematical reasoning is required to justify the underlying algorithm. Such reasoning can quickly go beyond the ability of automatic theorem provers. Proof assistants such as Isabelle and Coq provide an environment in which human users can guide the computer through the proof. However, such a process today often requires a lot of lowlevel reasoning with lists, sets, etc, as well as dealing with details of separation logic. We believe much work can still be done to provide more automation in this area, reducing the amount of time and expertise needed to perform verifications, with the goal of eventually making verification of complex algorithms a routine process.
The auto2 prover in Isabelle is introduced by the author in [28]. Its approach to automation in proof assistants is significantly different from the two main existing approaches: tactics and the use of external automatic theorem provers (as represented by Sledgehammer in Isabelle). Compared to Sledgehammer, auto2 is highly customizable: users can set up new reasoning rules and procedures at any point in the development of a theory (for example, our entire setup for separation logic is built outside the main auto2 program). It also works directly with higherorder logic and types available in Isabelle. Compared to tactics, auto2 uses a saturationbased search mechanism, that is closer to the kind of search performed in automatic theorem provers, and from experience has been more powerful and stable than the backtracking approach usual in the tactics framework.
In this paper, we apply auto2 to the verification of imperative programs. We limit ourselves to sequential programs with relatively simple memoryallocation patterns. The algorithms underlying the programs, however, require substantial reasoning to justify. The verification process can be roughly divided into two stages: verifying a functional version of the program, and refining it to an imperative version using separation logic.

We discuss the setup of auto2 to provide automation for both stages of this process. For the verification of functional programs, this means automatically proving simple lemmas involving lists, sets, etc. For refining to the imperative program, this means handling reasoning with separation logic.

Using our setup, we verify several data structures including redblack trees, interval trees, priority queues, and unionfind. We also verify algorithms including Dijkstra’s algorithm for shortest paths and a linesweeping algorithm for detecting rectangle intersection. These examples demonstrate that using our approach, complex algorithms can be verified in a highly efficient and modular manner.
We now give an outline for the rest of the paper. In Sect. 2, we give an overview of the auto2 prover. In Sect. 3, we discuss our setup of auto2 for verification of functional programs. In Sect. 4, we review the Imperative HOL framework in Isabelle and its separation logic, which we use to describe and verify the imperative programs. In Sect. 5, we discuss our setup of auto2 for reasoning with separation logic. In Sect. 6, we briefly describe each of the case studies, showing some statistics and comparison with existing verifications. Finally, we review related work in Sect. 7, and conclude in Sect. 8.
2 Overview of the auto2 Prover
The auto2 prover is introduced in [28]. In [29], several additional features are described, in an extended application to formalization of mathematics. In this section, we summarize the important points relevant to this paper.
Auto2 uses a saturationbased proof search mechanism. At any point during the search, the prover maintains a list of items, which may be derived facts, terms that appeared in the proof, or some other information. At the beginning, the statement to be proved is converted into contradiction form, and its assumptions form the initial state. The search ends successfully when a contradiction is derived. In addition to the list of items, the prover also maintains several additional tables, three of which will be described below.
2.1 Proof Steps
Proof steps are functions that produce new items from existing ones. During the development of an Isabelle theory, proof steps can be added or removed at any time. At each iteration of the proof search, auto2 applies the current list of proof steps to generate new items. Each new item is given a score and inserted into a priority queue. They are then added to the main list of items at future iterations in increasing order of score. The score is by default computed from the size of the proposition (smaller means higher priority), which can be overriden for individual proof steps.
Adding new proof steps is the main way to set up new functionality for auto2. Proof steps range from simple ones that apply a single theorem, to complex functions that implement some proof procedure. Several proof steps can also work together to implement some proof strategy, communicating through their input and output items. We will see examples of all these in Sects. 3 and 5.
2.2 Rewrite Table
Among the tables maintained by auto2, the most important is the rewrite table. The rewrite table keeps track of the list of currently known (ground) equalities. It offers two main operations: deciding whether two terms are equivalent, and matching up to known equalities (Ematching). The latter is the basic matching function used in auto2: whenever we mention matching in the rest of the paper, it is assumed to mean Ematching using the rewrite table.
We emphasize that when a new ground equality is derived, auto2 does not use it to rewrite terms in the proof state. Instead, the equality is inserted into the rewrite table, and incremental matching is performed on relevant items to discover new matches.
2.3 Property and WellFormedness Tables
We now discuss two other important tables maintained by auto2: the property table and the wellformedness table.
Any predicate (constant of type Open image in new window ) can be registered as a property during the development of a theory. During the proof, the property table maintains the list of properties satisfied by each term appearing in the proof. Common examples of predicates that we register as properties include sortedness on lists and invariants satisfied by binary search trees.
For any function, we may register certain conditions on its arguments as wellformedness conditions of that function. Common examples include the condition Open image in new window for the term Open image in new window , and Open image in new window for the term Open image in new window ( Open image in new window ’th element of the list Open image in new window ). We emphasize that registering wellformedness conditions is for the automation only, and does not imply any modification to the logic. During the proof, the wellformedness table maintains the list of wellformedness conditions that are known for each term appearing in the proof.
The property and wellformedness tables allow proof steps to quickly lookup certain assumptions of a theorem. We call assumptions that can be lookedup in this way side conditions. We will see examples of these in Sect. 3.1, and another important application of the wellformedness table in Sect. 3.2.
2.4 Case Analysis
The need for case analysis introduces further complexities. New case analysis is produced by proof steps, usually triggered by the appearance of certain facts or terms in the proof. We follow a saturationbased approach to case analysis: the list of cases (called boxes) is maintained as a part of the proof state, and derivation in all boxes are performed in parallel. More precisely, every item (and entry in the tables) is assigned to some box, according to the set of additional assumptions needed to derive that item. When a contradiction is derived in a box with additional assumption P, the fact \(\lnot P\) is added to its parent box. The proof finishes only if a contradiction is derived in the initial box (with no additional assumptions).
2.5 Proof Scripts
Auto2 defines its own language of proof scripts, which is similar to, but independent from the Isar proof language in Isabelle. The main differences between auto2 and Isar are that auto2 scripts do not contain names of tactics (all subgoals are proved using auto2), labels for intermediate goals, or names of previous theorems.
Examples of auto2 scripts are given in Sect. 3.4. We explain the basic commands here (all commands in auto2 scripts begin with an Open image in new window sign, to distinguish them from similar Isar commands).

Open image in new window : prove the intermediate goal P. Afterwards, make P available in the remainder of the proof block.

Open image in new window : prove the current goal with additional assumption P. Afterwards, make \(\lnot P\) available in the remainder of the proof block.

Open image in new window : here Open image in new window must be a fresh variable. Prove the intermediate goal Open image in new window . Afterwards, create variable x and make fact P(x) available in the remainder of the proof block.

Open image in new window : create a new proof block. That is, instead of proving the subgoal in the previous command directly using auto2, prove it using the commands between Open image in new window and Open image in new window .

Open image in new window , Open image in new window , etc: commands for several types of induction. Each type of induction has its own syntax, specifying which variable or proposition to apply induction on. We omit the details here.
3 Verification of Functional Programs
Proofs of correctness of functional programs involve reasoning in many different domains, such as arithmetic, lists, sets, maps, etc. The proof of a single lemma may require results from more than one of these domains. The design of auto2 allows automation for each of these domains to be specified separately, as a collection of proof steps. During the proof, they work together by communicating through the common list of items and other tables maintained by the prover.
In this section, we discuss our setup of auto2 for verification of functional programs. It is impossible to describe the entire setup in detail. Instead, we will give some examples, showing the range of functionality that can be supported in auto2. At the end of the section, we give an example showing the strength of the resulting automation.
We emphasize that the aim here is not to implement complete proof procedures, or to compete with highlyoptimized theory solvers for efficiency. Instead, we simply aim for the prover to consistently solve tasks that humans consider to be routine. Since we are in an interactive setting, we can always ask the user to provide intermediate goals for more difficult proof tasks.
3.1 Simple Proof Steps
Most of the proof steps added to auto2 apply a single theorem. Such proof steps can be added easily to auto2 (for example, a forward reasoning rule can be added by setting the Open image in new window attribute to a theorem). We describe some basic examples in this section.
Generating Case Analysis. Another class of proof steps generate case analysis on seeing certain terms or facts in the proof state. For example, there is a proof step that looks for terms of the form Open image in new window , and creates case analysis on Open image in new window for every match.
Case analysis may also be created to check wellformedness conditions. Usually, when we register a wellformedness condition, auto2 will look for the condition in the list of items during the proof. However, sometimes it is better to be more proactive, and try to prove the condition whenever a term of the given form appears. This is achieved by creating a case analysis with the condition as the goal (or equivalently, with the negation of the condition as the assumption).
3.2 Normalization of Natural Number Expressions
In this section, we give an example of a more complex proof step. It compares expressions on natural numbers by normalizing both sides with respect to addition and subtraction.
Mathematically, the expression \(ab\) on natural numbers is undefined if \(a<b\). In Isabelle (and many other proof assistants), it is simply defined to be zero. This means many equalities involving subtraction on natural numbers that look obvious are in fact invalid. Examples include \(ab+b=a\), which in Isabelle is false if \(a<b\).
This substantially complicates normalization of expressions on natural numbers involving subtraction. In general, normalization of such an expression agrees with intuition as long as the expression is wellformed, in the sense of Sect. 2.3. Following the terminology in [29, Sect. 3.3], we say a wellformed term is a term together with a list of theorems justifying its wellformedness conditions, and a wellformed conversion is a function that, given a wellformed term, returns an equality rewriting that term, together with theorems justifying wellformedness conditions on the right side of the equality. Wellformed conversions can be composed in the same way as regular conversions (rewriting procedures). In particular, we can implement normalization for expressions on natural numbers with respect to addition and subtraction as a wellformed conversion.
This is in turn used to implement the following proof step. Given any two terms s, t of type Open image in new window involving addition and subtraction, look for their wellformedness conditions in the wellformedness table. If all wellformedness conditions for subtraction are present, normalize s and t using the wellformed conversion. If their normalizations are the same, output the equality \(s = t\). Such proof steps, when combined with proof scripts, allow the user to rapidly perform arithmetic manipulations.
3.3 Difference Logic on Natural Numbers
Difference logic is concerned with propositions of the form \(a\le b + n\), where n is a constant. A collection of such inequalities can be represented as a directed graph, where nodes are terms and weighted edges represent inequalities between them. A collection of inequalities is contradictory if and only if the corresponding graph contains a negative cycle, which can be determined using the BellmanFord algorithm.
In auto2, we implement difference logic for natural numbers using special items and proof steps. While less efficient than a graphbased implementation, it is sufficient for our purposes, and also interacts better with other proof steps. Each inequality on natural numbers is represented by an item of type Open image in new window , which contains a triple Open image in new window recording the terms on the two sides and the difference. The transitivity proof step looks for pairs of items of the form Open image in new window and Open image in new window , and produces the item Open image in new window for each match. The resolve proof step looks for items of the form Open image in new window , where Open image in new window is less than zero, and derives a contradiction for each match.
3.4 Example
The only hints that needs to be provided by the human to prove these lemmas are how to apply the induction (specified using the Open image in new window command). By comparison, in the AFP library [14], the corresponding proofs require 20 tactic invocations in 42 lines of Isar text.
4 Imperative HOL and Its Separation Logic
In this section, we review some basic concepts from the Imperative HOL framework in Isabelle and its separation logic. See [3, 13, 14] for details.
4.1 Heaps and Programs
In Imperative HOL, procedures are represented as Haskellstyle monads. They operate on a heap (type Open image in new window ) consisting of a finite mapping from addresses (natural numbers) to natural numbers, and a finite mapping from addresses to lists of natural numbers (in order to support arrays). Values of any type Open image in new window can be stored in the heap as long as one can specify an injection from Open image in new window to the natural numbers. This means records with multiple fields, such as nodes of a search tree, can be stored at a single address. Along with native support for arrays, this eliminates any need for pointer arithmetic.
4.2 Assertions and Hoare Triples
The type partial heap is defined by Open image in new window . The partial heap (h, as) represents the part of the heap h given by the set of addresses as.
An assertion (type Open image in new window ) is a mapping from Open image in new window to Open image in new window , that does not depend on values of the heap outside the address set. The notation \((h, as) \vDash P\) means “the assertion P holds on the partial heap (h, as)”.

Open image in new window : holds for all valid partial heaps.

Open image in new window : the partial heap is empty.

\(\uparrow (b)\): the partial heap is empty and b (a boolean value) holds.

\(p\mapsto _ra\): the partial heap contains a single address pointing to value a.

\(p\mapsto _axs\): the partial heap contains a single address pointing to list xs.
5 Automation for Separation Logic
In this section, we discuss our setup of auto2 for separation logic. The setup consists of a collection of proof steps working with Hoare triples and entailments, implemented in around 2,000 lines of ML code (including specialized matching for assertions). While knowledge of auto2 is necessary to implement the setup, we aim to provide an easytounderstand interface, so that no knowledge of the internals of auto2, or of details of separation logic, is needed to use it for concrete applications.
5.1 Basic Approach
Our basic approach is to analyze an imperative program in the forward direction: starting at the first command and finishing at the last, using existing Hoare triples to analyze each line of the procedure. To simplify the discussion, suppose the procedure to be verified consists of a sequence of commands \(c_1; \ldots ; c_n\). Let \(P_0\) be the (spatial) precondition of the Hoare triple to be proved.
 1.
Match the pattern c with the command \(c_1\), instantiating some of the arbitrary variables in the Hoare triple.
 2.
Match the spatial part of the precondition with \(P_0\). This is the frameinference step: the matching is up to the associativecommutative property of separating conjunction, and only a subset of factors in \(P_0\) need to be matched. Each match should instantiate all remaining arbitrary variables in the Hoare triple.
 3.
Generate case analysis (discussed at the end of Sect. 3.1) to try to prove each of the pure conditions \(a_i\).
 4.
After all pure conditions are proved, apply the Hoare triple. This creates new variables for the return value r and possible data variables \(\mathbf {x}\). The procedure is replaced by \(c_2;\dots ;c_n\) and the precondition is replaced by Open image in new window . The pure assertions \(b_1,\dots ,b_l\) in the postcondition are outputed as facts.
On reaching the end of the imperative program, the goal reduces to an entailment, which is solved using similar matching schemes as above.
5.2 InductivelyDefined Assertions
We follow the policy of always using assertions in the more expanded form (that is, (1) instead of (2)). This means matching of assertions must also take into account inductive definitions of assertions, so that the assertion (1) will match the pattern Open image in new window as well as (for example) the pattern Open image in new window . This is realized by maintaining a list of inductive definitions of assertions in the theory, and have the special matching function for assertions refer to this list during matching.
5.3 Modularity
For any data structure, there are usually two levels at which we can define assertions: the concrete level with definition by induction or in terms of simpler data structures, and the abstract level describing what data the structure is supposed to represent.
After the Hoare triples for Open image in new window are proved, the definition of Open image in new window , as well as the Hoare triples for Open image in new window , can be hidden from auto2 by removing the corresponding proof steps. This enforces modularity of proofs: auto2 will only use Hoare triples for Open image in new window from now on, without looking into the internal implementation of the binary tree.
5.4 Example
Note that the imperative procedure performs full compression along a path, rather than a single compression for the functional version in Sect. 3.4. By comparison, the corresponding proof in the AFP requires 13 tactic invocations (including 4 invocations of Open image in new window ) in 34 lines of Isar text.
6 Case Studies
#Imp  #Def  #Thm  #Step  Ratio  #LOC  

Unionfind  49  7  26  42  0.86  244 
Redblack tree  270  27  83  173  0.64  998 
Interval tree  84  17  50  83  0.99  520 
Rectangle intersection  33  18  31  111  3.36  417 
Indexed priority queue  83  10  53  84  1.01  477 
Dijkstra’s algorithm  44  19  62  150  3.41  549 

#Imp is the number of lines of imperative code to be verified.

#Def is the number of definitions made during the verification (not counting definitions of imperative procedures).

#Thm is the number of lemmas and theorems proved during the verification.

#Step is the number of “steps” in the proof. Each definition, lemma, and intermediate goal in the proof script counts as one step (so for example, a lemma proved with one intermediate goal counts as two steps). We only count steps where auto2 does some work, omitting for example variable definitions.

Ratio: ratio between #Step and #Imp, serving as a measure of the overhead of verification.

#LOC: total number of lines of code in the theories (verification of functional and imperative program). This can be used to make approximate comparisons with other work.
6.1 UnionFind
Our verification follows closely that in the AFP [14]. As in the example in the AFP, we do not verify that the array containing the size of components has reasonable values (important only for performance analysis). Two snippets of auto2 proofs are shown in previous sections. Overall, we reduced the number of lines in the theory by roughly a half. In a further example, we applied unionfind to verify an algorithm for determining connectivity on undirected graphs (not counted in the statistics).
6.2 RedBlack Tree
We verified the functional redblack tree given by Okasaki ([21], for insertion) and Kahrs ([18], for deletion). Both functional correctness and maintenance of invariants are proved. We then verified an imperative version of the same algorithm (imperative in the sense that no more memory is allocated than necessary). This offers a stringent test for matching involving inductively defined assertions (discussed in Sect. 5.2). For the functional part of the proof, we used the technique introduced by Nipkow [19] for proving sortedness and proper behavior on the associated maps using the inorder traversal as an intermediary.
Functional redblack tree has been verified several times in proof assistants [2, 19]. The imperative version is a common testcase for verification using automatic theorem provers [17, 22, 23, 24]. It is also verified “autoactively” in the SPARK system [9], but apparently not in proof assistants such as Coq and Isabelle.
6.3 Interval Tree and Rectangle Intersection
Interval tree is an augmented data structure, with some version of binary search tree serving as the base. It represents a set of intervals S, and offers the operation of determining whether a given interval i intersects any of the intervals in S. See [8, Sect. 14.3] for details. For simplicity, we verified interval tree based on an ordinary binary search tree.
As an application of interval trees, we verify an algorithm for detecting rectangle intersection (see [8, Exercise 14.37]). Given a collection S of rectangles aligned to the x and y axes, one can determine whether there exists two rectangles in S that intersect each other using a linesweeping algorithm as follows. For each rectangle \([a,b]\times [c,d]\), we create two operations: adding the interval [a, b] at time c, and removing it at time d. The operations for all rectangles are sorted by time (breaking ties by putting insertion before deletion) and applied to an initially empty interval tree. There is an intersection if and only if at some point, we try to insert an interval which intersects an existing interval in the tree. Formal verification of interval trees and the linesweeping algorithm for rectangle intersection appear to be new.
6.4 Indexed Priority Queue and Dijkstra’s Algorithm
The usual priority queue is implemented on one array. It supports insertion and deleting the minimum. In order to support decreasing the value of a key (necessary for Dijkstra’s algorithm), we need one more “index” array recording locations of keys. Having two arrays produce additional difficulty in having to verify that they stay in sync in all operations.
The indexed priority queue is applied to verify a basic version of Dijkstra’s algorithm. We make several simplifying assumptions: the vertices of the graph are natural numbers from 0 to \(n1\), and there is exactly one directed edge between each ordered pair of vertices, so that the weights of the graph can be represented as a matrix. Since the matrix is unchanged during the proof, we also do not put it on the heap. Nevertheless, the verification, starting from the definition of graphs and paths, contains all the essential ideas of Dijkstra’s algorithm.
The indexed priority queue and Dijkstra’s algorithm are previously verified using the refinement framework in [12, 20]. It is difficult to make precise comparisons, since the approach used in the refinement framework is quite different, and Dijkstra’s algorithm is verified there without the above simplifying assumptions. By a pure line count, our formalization is about 23 times shorter.
7 Related Work
This paper is a continuation of the work in [28, 29]. There is already some verification of imperative programs in [28]. However, they do not make use of separation logic, and the examples are quite basic. In this paper, we make full use of separation logic and present more advanced examples.
The refinement framework, introduced by Lammich in [13], can also be used to verify programs in ImperativeHOL. It applies refinement and data abstraction formally, verifying algorithms by stepwise refinement from specifications to concrete implementations. It has been used to verify several advanced graph algorithms [11, 15, 16]. Our work is independent from the refinement framework. In particular, we use refinement and data abstraction only in an adhoc manner.
Outside ImperativeHOL, there are many other frameworks based on tactics for automating separation logic in proof assistants. Examples include [1, 4, 5, 6, 7, 14, 27]. As discussed in the introduction, our framework is implemented on top of the auto2 prover, which follows a quite different approach to automation compared to tactics.
Finally, there are many systems for program verification using automatic theorem provers. The main examples include [10, 25, 26]. The basic approach is to generate verification conditions from usersupplied annotations, and solve them using SMTbased provers. Compared to such systems, we enjoy the usual advantages of working in an interactive theorem prover, including a small trusted kernel, better interaction when proving more difficult theorems, and having available a large library of mathematical results.
8 Conclusion
In this paper, we described the setup of the auto2 prover to provide automation for verification of imperative programs. This include both the verification of a functional version of the program, and refining it to the imperative version using separation logic. Using our framework, we verified several data structures and algorithms, culminating in Dijkstra’s shortest paths algorithm and the linesweeping algorithm for detecting rectangle intersection. The case studies demonstrate that auto2 is able to provide a great deal of automation in both stages of the verification process, significantly reducing the length and complexity of the proof scripts required.
Footnotes
 1.
Code available at https://github.com/bzhan/auto2.
Notes
Acknowledgements
The author would like to thank Adam Chlipala, Peter Lammich, and Tobias Nipkow for discussions and feedback during this project, and to the referees for their helpful comments. For the first half of this project, the author was at MIT and was supported by NSF Award No. 1400713. During the second half, the author is at TU Munich, and is supported by DFG Koselleck grant NI 491/161.
References
 1.Appel, A.: Tactics for separation logic, January 2006. http://www.cs.princeton.edu/~appel/papers/septacs.pdf
 2.Appel, A.: Efficient verified redblack trees (2011). http://www.cs.princeton.edu/~appel/papers/redblack.pdf
 3.Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540710677_14CrossRefGoogle Scholar
 4.Cao, J., Fu, M., Feng, X.: Practical tactics for verifying C programs in Coq. In: Leroy, X., Tiu, A. (eds.) CPP 2015, pp. 97–108 (2015)Google Scholar
 5.Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: ICFP, pp. 418–430. ACM (2011)Google Scholar
 6.Chlipala, A.: Mostlyautomated verification of lowlevel programs in computational separation logic. In: PLDI 2011, pp. 234–245 (2011)CrossRefGoogle Scholar
 7.Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higherorder imperative programs. In: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009), pp. 79–90, August 2009Google Scholar
 8.Cormer, T.H., Leiserson, C.E., Rivest, R., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (1989)Google Scholar
 9.Dross, C., Moy, Y.: Autoactive proof of redblack trees in SPARK. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 68–83. Springer, Cham (2017). https://doi.org/10.1007/9783319572888_5CrossRefGoogle Scholar
 10.Filliâtre, J.C., Paskevich, A.: Why3 — Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642370366_8CrossRefGoogle Scholar
 11.Lammich, P.: Verified efficient implementation of Gabow’s strongly connected component algorithm. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 325–340. Springer, Cham (2014). https://doi.org/10.1007/9783319089706_21CrossRefGoogle Scholar
 12.Lammich, P.: Refinement based verification of imperative data structures. In: Avigad, J., Chlipala, A. (eds.) CPP 2016, pp. 27–36 (2016)Google Scholar
 13.Lammich, P.: Refinement to imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253–269. Springer, Cham (2015). https://doi.org/10.1007/9783319221021_17CrossRefGoogle Scholar
 14.Lammich, P., Meis, R.: A separation logic framework for imperative HOL. In: Archive of Formal Proofs, November 2012. http://afp.sf.net/entries/Separation_Logic_Imperative_HOL.shtml. Formal proof development
 15.Lammich, P., Sefidgar, S.R.: Formalizing the EdmondsKarp algorithm. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 219–234. Springer, Cham (2016). https://doi.org/10.1007/9783319431444_14CrossRefGoogle Scholar
 16.Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166–182. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642323478_12CrossRefGoogle Scholar
 17.Le, Q.L., Sun, J., Chin, W.N.: Satisfiability modulo heapbased programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part I. LNCS, vol. 9779, pp. 382–404. Springer, Cham (2016). https://doi.org/10.1007/9783319415284_21CrossRefGoogle Scholar
 18.Kahrs, S.: Redblack trees with types. J. Funct. Program. 11(4), 425–432 (2001)CrossRefGoogle Scholar
 19.Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 307–322. Springer, Cham (2016). https://doi.org/10.1007/9783319431444_19CrossRefGoogle Scholar
 20.Nordhoff, B., Lammich, P.: Formalization of Dijkstra’s algorithm. Archive of Formal Proofs, January 2012. https://www.isaafp.org/entries/Dijkstra_Shortest_Path.html
 21.Okasaki, C.: Redblack trees in a functional setting. J. Funct. Program. 9(4), 471–477 (1999)CrossRefGoogle Scholar
 22.Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: PLDI 2014, pp. 440–451 (2014)CrossRefGoogle Scholar
 23.Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711–728. Springer, Cham (2014). https://doi.org/10.1007/9783319088679_47CrossRefGoogle Scholar
 24.Qiu, X., Garg, P., Ştefănescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI 2013, pp. 231–242 (2013)CrossRefGoogle Scholar
 25.Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642175114_20CrossRefzbMATHGoogle Scholar
 26.Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical report CW520, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, August 2008Google Scholar
 27.Tuerk, T.: A separation logic framework for HOL. Technical report UCAMCLTR799, University of Cambridge, Computer Laboratory, June 2011Google Scholar
 28.Zhan, B.: AUTO2, a saturationbased heuristic prover for higherorder logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 441–456. Springer, Cham (2016). https://doi.org/10.1007/9783319431444_27CrossRefGoogle Scholar
 29.Zhan, B.: Formalization of the fundamental group in untyped set theory using auto2. In: AyalaRincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 514–530. Springer, Cham (2017). https://doi.org/10.1007/9783319661070_32CrossRefGoogle Scholar
Copyright information
<SimplePara><Emphasis Type="Bold">Open Access</Emphasis> This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.</SimplePara> <SimplePara>The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.</SimplePara>