General methods : assertions, rewriting, abstract interpretation, logics and proof assistants

In 1963, in a seminal article championing the mathematical treatment of programming and introducing a remarkable array of new concepts, J. McCarthy introduced the very different idea of using term rewriting as a tool applicable to both program optimization and formal verification. This approach, the second we'll be studying, has had a long descent into verification systems (Boyer&More, ACL2, PVS, Key, ProVerif, etc.), and continues to irrigate other approaches. It has had remarkable success in circuits, avionics, security, etc.

The third historical approach is that of denotational language semantics, introduced by Scott and Strachey around 1970. Here, a program is interpreted as a function in a topological space ordered by information order, and all functions are made total by the explicit addition of indefinite elements. A general theory of fixed points in ordered spaces provides a uniform interpretation of loops, recursion and higher-order functional programming. In the early 1970s, this theory was the basis of the pioneering program proof assistant, LCF, created by Milner et al. But explicit treatment of the indefinite proved too complicated, and proof assistants subsequently took a different path. Denotational semantics did, however, have considerable success in another approach to verification, abstract interpretation, created by P. and R. Cousot in 1977. The idea here is to work with assertions that no longer relate to the exact values calculated, but to an abstraction of them, as the proof by 9 does to detect errors in multiplication. Numerous abstract domains have been developed, along with general algorithmic methods for combining these domains and accelerating fixed-point calculations. Abstract interpretation is now developed industrially. It has been used to verify critical properties of very large programs, such as the absence of runtime errors in the Airbus A380 pilot code. It is also used to evaluate the maximum computation time of embedded software and to accelerate computations in other types of verification systems.

The fourth approach covered in this lecture is verification using logical proof assistants. The idea here is to translate the computer verification problem into a purely logical one, and to provide verification assistance through a system of tactics and man-machine interaction to organize logical proofs on a large scale, augmented by partial automations for specific sub-domains using, for example, rewriting techniques. Current wizards cover a wide range of logic types, from first-order predicate calculi augmented by set theory (Rodin for Event B, etc.) or temporal logic (TLA+), to higher-order calculi (HOL, Isabelle, Coq, etc.). This lecture will briefly introduce first-order workshops, with higher-order ones covered in the following lecture. We'll take the example of J.-R. Abrial's B and Event-B formalisms (speaker at the last seminar on April^1, 2015). Workshop B has been used for the specification, programming and formal verification of critical software for the operation of the RER A, line 14 (Meteor) of the Paris metro, and several other railway systems. Event-B and its Rodin system are an evolution of B towards event-driven systems, which are ubiquitous in embedded computing.