J. Brauer and A. Simon. Inferring Definite Counterexamples Through Under-Approximation. In A. E. Goodloe and S. Person, editors, NASA Formal Methods, volume 7226 of LNCS, Norfolk, Virginia, USA, April 2012. Springer.

Abstract interpretation for proving safety properties summarizes concrete traces into abstract states, thereby trading the ability to distinguish traces for tractability. Given a violation of a safety property, it is thus unclear which trace led to the violation. Moreover, since part of the abstract state is over-approximate, such a trace may not exist at all. We propose a novel backward analysis that is based on abduction of propositional Boolean logic and that only generates legitimate traces that reveal actual defects. The key to tractability lies in modifying an existing projection algorithm to stop prematurely with an under-approximation and by combining various algorithmic techniques to handle loops finitely.

Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com