Principles of Abstract Interpretation: By Patrick Cousot MIT Press, 2021, ISBN 9780262044905, pp. 1–819. Reviewed by Reinhard Wilhelm

Some years ago, the author of the reviewed book and the author of the review shared a ride in the shuttle from Grenoble to Lyon Airport. The author-to-be told the reviewer-to-be about the state of his book project. The existing draft had 1,000 pages. The reviewer explained to the author that in his deep insight into the nature of things and his long-term experience with textbooks there were books that improve the world and there were books that are being read. The author asked for confirmation whether the reviewer felt that the coming book would belong to those books that improve the world. Let me skip how I got myself out of this difficult situation. When asked whether a book will be read, the question is by whom. Citing the author, this book is intended for readers interested in the theory of abstract interpretation, the understanding of formal methods, and the design of verifiers and static analyzers. And my answer is, it is a must read for these groups of people.

To make one thing clear from the beginning: This reviewer need not be convinced of the value of Abstract Interpretation as his greatest scientific achievements [5, 6, 8, 10] are based on the foundational work on Abstract Interpretation by Patrick and Radhia Cousot.

Static analyses are distinct from …model checking, which verifies the correctness of a separate external specification of a program [9]. In model checking, a user supplies the program to be verified and the logical expression or the automaton against which the program is to be checked at the same time. In static analysis there are distinct times, a time when an abstract interpreter is designed with certain facts in mind to be extracted from a class of programs, and there is a time when the abstract interpreter is applied by programmers or verification engineers to extract these type of facts from particular programs. This enables a fruitful division of work. The first phase, the design of non-trivial abstract interpreters needs highly competent specialists, while the second phase is easier, although sometimes also non-trivial. The designer needs to identify abstract domains to represent these facts and transfer functions for the expressions or statements of the considered programming language that describe the transformation of facts by evaluating the expression or executing the statement. The book provides many ways to construct abstract domains for different static analyses, numerical as well as symbolic abstract domains. So, it is mainly written for the designers of abstract interpreters and researchers in formal methods to whom it provides an excellent mathematical foundation. Nowhere else are the foundations of sound static program analyses presented in such depth, breadth, and beauty, in particular the relation to programming-language semantics, which provides for many static analyses to be correct by construction.

This relation actually has been the inspiration of the work developing Abstract Interpretation by Patrick and Radhia Cousot. Compiler writers were using what they called Data Flow Analysis to compute applicability conditions for optimizing program transformations. However, these Data Flow Analyses lacked the relation to the semantics of the programming language, which would have been necessary to prove their correctness and thus correctness preservation of the program transformations. In Patrick’s dissertation and a sequence of POPL papers [1, 2, 3, 4] the Cousots and their students clarified this relation. This important relation to the programming language is introduced gently in Chapter 3 of the book using simple examples like statically computing the signs of expressions. Much of the correctness proofs in the book are based on Trace Semantics, which are introduced and thoroughly treated in Part III. Trace semantics are essential for understanding many static analyses [7]. Part IV, entitled Properties and their Abstraction, lays the foundation for the central notion of Abstraction. Abstraction, concretization, and their interaction in the computation of fixedpoints are the important ingredients of Abstract Interpretation. Fixedpoints and their abstractions are treated in Part V. The semantics of a programming language is abstracted into an abstract domain and an abstract interpreter in Part VII. This is a generic static analysis parameterized with an abstract domain. Particular abstract domains, numeric, relational, and symbolic abstract domains are developed in Parts IX, XI, and XII. Some sound static-analysis tools are described in Part XIV. An extensive bibliography concludes the book.

This book is Patrick Cousot’s opus maximum, a treasure for the researcher on formal methods.