Today, advanced logics are often formulated as variations on the theme of “higher-order concurrent separation logic.” One of these, Verifiable C, is the foundation of Appel’s Verified Software Toolchain, 1 and includes an expressive higher-order logic supporting recursive predicates. Iris29 encompasses reasoning about fine-grained concurrency and even relaxed memory, based on different instantiations of a single generic model. Iris has been used to provide a foundation of the type system of the Rust programming language, 28 which is very natural when you consider that ownership transfer is one of the central ideas in Rust.

Technically, these works are based on “non-standard models” of SL, different from the heaplet model but instances of Pym’s resource semantics as in Figure 2; see Pym et al. 36 There are many such models, including ones incorporating read and other permissions, 7 auxiliary state, 39 time, 39 protocols, 29 and others. Abstract SL13 showed how general program logic could be defined based on these models, and the works just mentioned and others showed that some of them had surprising ramifications.

Fictional separation and views worked to reimagine fundamental concepts. The programs being proven go beyond the loosely connected processes that CSL was originally designed for. Significant new theoretical insights and soundness arguments were needed to justify the program-proof rules supporting the fine-grained concurrency examples. 17 This led to a flowering of interest and new ideas which is still in progress. A recent survey on CSL provides many more references in addition to those mentioned here. 9

Directions in
Mechanized Reasoning

SL spawned new approaches to verification tools. In order to provide a taste of where the field has gone, we present a sampling of practical achievements; that is, we focus on the end points rather than the (important) advancements along the way that helped get there. Further references to the literature, including discussion on intermediate advances, may be found in the appendix ( https://bit.ly/2CQD9CU).

Mostly automatic verification. Small-
foot, 2 from Calcagno, Berdine, and
O’Hearn, was the first SL verification
tool. Given procedure pre/post specs,
loop invariants and invariants governing
lock usage, Smallfoot attempts to con-
struct a proof. For the pointer-transfer-
ring buffer, given a buffer invariant and
pre/post specs for put and get it can
verify memory safety and race freedom.

Smallfoot used a decidable fragment of SL dubbed “symbolic heap,” formu-lae of the form B ∧ H where H is a separating conjunction of heap facts and B is a Boolean assertion over non-heap data. The format was chosen to make in-place symbolic execution efficient. Smallfoot’s heap facts were restricted to points-to assertions, linked lists and trees. Subsequent works extended symbolic heaps in numerous directions, covering more inductive definitions as well as arrays and arithmetic; see appendix ( https://bit.ly/2CQD9CU).

Some of the most substantial automatic verifications done with SL have been carried out with the VeriFast tool of Jacobs and colleagues. VeriFast employs a symbolic execution engine like Smallfoot, but integrates a dedicated SL theorem prover with a classical SMT solver for non-heap data. A paper reports on the verification of several industrial case studies, including Java Card programs and device drivers written in C; 35 see VeriFast’s GitHub site for these and many other examples ( https://github.com/ verifast/verifast).

Interactive verification. In an automatic verifier like Smallfoot, the proof construction is automatic, given the pre/post annotations plus invariants. In interactive verification the human helps guide the proof search, commonly using a proof assistant such as Coq, HOL4, or Isabelle. Interactive verification can often prove stronger properties than automatic verifiers, but the cost is higher.

Interactive verifiers have been used to prove small, intricate algorithms. A recent paper reports on the verification of low-level concurrent algorithms including a CAS-lock, a ticketed lock, a GC allocator, and a non-blocking stack. 39 An emphasis is placed on reusability; for instance, the stack uses the GC allocator, which in turn uses a lock, but the stack uses the spec of the allocator and the allocator uses the spec rather than the implementation of a lock.

The verifiable C logic1 has been
used to prove crypto code. For example,
OpenSSL’s HMAC authentication code,
comprising 134 lines of C, was proven
using 2,832 lines of Coq. 4

A larger example is the FSCQ file system. 14 The code and the proof are both done in Coq, taking up 31k lines of proof+code. This compares to 3k lines of C for a related unverified file system. Although the initial effort, which included development of a program logic framework in Coq, took several person years, experiments show incremental, lower cost when modifying code+proof.

A commercial example concerns key modules of a preemptive OS kernel, the μC/OS-II. 41 Modules verified include the scheduler, interrupt handlers, and message queues. 1.3k lines of C were proven using 216k lines of Coq. It took four person years to develop the framework, one-person year to prove the first module, and then the remaining modules, around 900 lines of C, took six person-months.

Automatic program analysis. With a verification-oriented program analysis the annotations that a human would supply to a mostly automatic verifier like Smallfoot—invariants and pre/post specs—are inferred. A tool will be able to prove weaker properties when the human is not supplying annotations, but can more easily be deployed broadly to many programmers.

Program analysis with SL has received a great deal of attention. At first, analysis was formulated for simple linked lists, 20 and progressively researchers moved on to more involved data structures. A practical high point in this line of work was the verification of pointer safety in Linux and Windows device drivers up to 10k LOC by the SpaceInvader program analyzer. 43 SpaceInvader was an academic tool; its sibling, SLAyer, 3 developed in parallel at Microsoft, was used internally to find 10s of memory safety errors in Windows device drivers. SpaceInvader and SLAyer were able to analyze complex, linear data structures: for example, oneWindows driver manipulated five-cyclic doubly linked lists sharing a common header node, three of which had acyclic sublists.

Like much research in verification-oriented program analysis these techniques worked in a whole-program fashion: you start from main() or