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.