Re-Engineering Abstract Interpretation

Abstract:

Abstract Interpretation is widely recognized as a sound basis for doing whole program static analysis. Abstract Interpretation has classically been based on representing the values of program variables using abstract domains with appropriate widening operators to allow the set of possible abstract states at every program point to reach a fixed point. There are a number of challenges with this approach when the number of program variables is large, in that the representation of the set of possible abstract states is necessarily complex. To reduce the level of complexity in the representation of the state of a combination of related variables, we have taken an unconventional approach, based on "value numbering." We convert the program to a "static-single-assignment" (SSA) representation and then perform a global value numbering. Subsequent analysis is performed over possible value sets associated with each value number.

The net effect of this approach is that we are able to efficiently and precisely analyze whole programs, propagating inferred contracts bottom-up through the call tree, and iterating to a fixed-point over the whole program in the case of recursion. This technology forms the basis for the commercial CodePeer static analysis tool from AdaCore, and has demonstrated advantages in scalability and precision over more conventional abstract interpretation approaches, while generating as-built documentation in the form of inferred contracts to support code review.

Biography:

S. Tucker Taft is VP and Director of Language Research at AdaCore, a company focused on open-source tools to support the development of high-integrity software. Tucker joined AdaCore in 2011 as part of a merger with SofCheck, a company he had founded in 2002 to develop advanced static analysis technology. Prior to that Tucker was a Chief Scientist at Intermetrics, Inc. and its follow-ons for 22 years, where in 1990-1995 he led the design of Ada 95. Tucker received an A.B. Summa Cum Laude degree from Harvard University, where he has more recently taught compiler construction and programming language design.