Abstract: Traditional software model-checkers build over-approximating abstractions of the programs they analyze and typically bias their analysis towards proving that a (safety) property of interest holds (verification). On the other hand, since model-checkers are widely known for their bug-finding abilities, they are often used for refutation. In this case, the above approach seems unreasonable: why introduce spurious behavior and make it more difficult to find a real bug? For such circumstances, one would just want to prove that the property is false (refutation), without necessarily building a witness for that.

In this talk, I will present YASM -- a symbolic software model-checker based on exact abstraction that combines over- and under-approximating abstractions in a single model. YASM can prove and disprove properties with equal effectiveness. Our experiments show that performance of the tool is comparable with standard over-approximating model-checkers. The implementation makes use of a number of ideas from the existing approaches to Counterexample Guided Abstraction Refinement (CEGAR), which we have generalized for our purposes. More importantly, minor modifications of the CEGAR framework enable an array of useful analyzes, such as analyzing programs with non-deterministic control flow, reasoning about arbitrary CTL properties, reusing previously computed abstractions, and many others.

Arie Gurfinkel is a PhD candidate in the Department of Computer Science at the University of Toronto and is expected to graduate in the Spring of 2007. He has recently joined the Software Engineering Institute at Carnegie-Mellon University as a Member of the Technical Staff. He has received a B.Sc. and a M.Sc. degrees in computer science from the University of Toronto, in 2000 and 2003, respectively. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated techniques for program verification. Arie has received an NSERC Postgraduate Scholarship in 2003, and an IBM Ph.D. Fellowship in 2004. In the summer of 2005, he completed an internship at IBM CAS Toronto, where he worked on integrating a software model-checker YASM within the Eclipse IDE, and explored static and dynamic approaches for analysis of web services. Appointments: dcm@cs.cmu.edu