# Abstractions from proofs (@ POPL 2004)

### Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan

This is a seminal paper in formal verification. It describes how to use Craig Interpolants to speed-up the verification of imperative program properties. The high-level idea is nice. I went up to somewhere in page 5 in detail with a friend. You have your program, of which you're trying to prove some property. Traditionally, static analysis over-approximate the space state of the programs to be practical, but that means they have false positives: the analysis might say "you program has a bug, because if $P$ happens, then you will access this invalid pointer", for example. But it might be the case that $P$ is actually impossible. On the other hand, it is difficult to get precise analyses (i.e. those that do not give false positives) to scale to large programs. One specific challenge is that, in order to prove that a trace of execution is impossible, your verifier might need to remember an exponential number of facts about the program when it's following possible traces of execution. In order to prove that a trace is infeasible, your SMT solver might use facts points of the program that are very early on. In order to only need smaller, more local predicates, they use Craig Interpolants.