Don’t go near this paper unless you are familiar with the Nelson-Oppen method, satisfiability modulo theories (SMT), first-order logic, complete partial orders (CPOs), Tarski, monotone Galois connections, formal semantics, and a host of other abstractions. Otherwise, visit the Astrée website [1] to see what this research has achieved in practice--it is impressive.

The paper summarizes 40 years of research in 56 pages of rigorously argued logic and mathematics. The authors propose combining algebraic and model theoretic methods with the logical and proof theoretic approach using SMT to make an efficient and expressive way to prove program properties. It would be more convincing if the proofs and definitions in the paper had been syntax checked, as there are some errors, such as missing parentheses, for example. An example shows the discovery of a bounds error in a C program, but the theory of arrays in C is not in the paper. I would like to see the theory extended to apply to programs that include “while” and “if” statements, subprograms, or polymorphism.