Astrée). The abstraction of Astrée is designed by conjunction of many elementary abstractions that are individually simple to understand and implement. In the case of a false alarm, each abstraction can be adjusted in cost and precision by parameters and abstraction directives (whose inclusion in the code can be automated). If the false alarm cannot be solved by the existing abstractions, new abstractions can be easily incorporated to extend and refine the conjunction of abstractions. The abstract invariants can therefore be strengthened in a few refinement steps until no false alarm is left. ⁷

Byron cook:
Verification of concurrent systems

Many critical applications involve high degrees of concurrency, whereby a number of activities progress in parallel with each other. Concurrency can create surprisingly complex interactions among the concurrent components, making the verification problem inherently more complex.

The traditional methods of specifying and automatically reasoning about computer systems are not sufficient for use with concurrent systems. They do not allow for the side effects caused by other concurrent components, the occurrence of multiple simultaneous events, or the synchronization required between processes to ensure data integrity, and so forth. Specialized tools will normally be required for effective verification.

As an example, consider thread termination. Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Such functions can be found in operating systems, Web servers, and email clients. Until now, no known automatic program termination prover supported a practical method of proving the termination of threads.

As another example, concurrent programs are usually written in languages that assume but do not guarantee memory safety (such as, pointer dereferences never fail, and memory is never leaked). Again, until now, no known automatic program verifier supported the proving of memory safety for concurrent programs.

Recent advances now allow us to address these problems (such as, proving

BYRon cooK
concurrency
can create
surprisingly
complex
interactions
among the
concurrent
components,
making the
verification
problem
inherently
more complex.

properties such as memory safety and termination of concurrent code. These advances have led to the recently added support for concurrency in the Terminator termination prover¹⁵ and the SLAyer shape analysis engine. ¹⁴

The common theme of these advances is thread modularity: existing sequential-program provers can be used to prove the correctness of concurrent programs if appropriate abstractions can be found to represent the other threads in a concurrent system. In the case of termination proving, the abstractions describe the direction of change (called the variance) of values caused by the other threads in the system. We might know, for example, that the value of the variable x cannot go up in the other threads, thus allowing us to prove the termination of a loop in the thread of interest that decrements x during each loop iteration. In the case of memory-safety proving, the abstractions describe the association between locks and data structures: we can prove the memory safety of the thread of interest by assuming that certain data structures are safe to modify only when the associated locks are acquired.

The difficulty with thread-modular techniques is that the space of abstractions is so large that finding the right one for a given program verification problem is difficult. Heuristics must be developed. Furthermore, through the use of experimental evaluations, these heuristics must be shown to work in the common case. We have developed and evaluated such heuristics. In the case of termination proving, we have found that by temporarily ignoring concurrency we can guess a set of ranking functions (see Patterson¹³ for details), which leads to a useful candidate abstraction. Using static program analysis techniques we can prove, for example, that every instruction in the other threads does not increment x. The fact that x needs not to be incremented, as opposed to y, comes from the proof of termination via the sequential-program termination prover (see Cook⁴ for the details).

In the case of proving memory safety, we use initial guesses that match locks to variables, and then use counterex-ample-guided techniques to refine the shape of the data structures protected by the locks (see Gotman⁹ for further details).