Distinguishing paths (for fun and profit)

David Monniaux ( CNRS, VERIMAG )

Static analysis by abstract interpretation usually implements joins in the control-flow graph by some kind of "least upper bound" operation. Unfortunately, this may introduce spurious states, resulting in true properties not being provable. A workaround is to distinguish individual paths inside loops, but this leads to exponential blowup. Here we present techniques combining SMT-solving and abstract interpretation.

Joint work with Thomas Gawlitza, Laure Gonnord and Julien Henry.