Distinguishing paths (for fun and profit) (joint work with Thomas Gawlitza, Laure Gonnord and Julien Henry) 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.