The Quest for Systematic Predicate Abstraction

by Philipp Ruemmer

Abstract
Heuristics for discovering predicates for abstraction are an essential part of CEGAR-based software model checkers or Horn solvers. Picking the right predicates affects the runtime of a model checker, or determines if a model checker is able to solve a verification task at all. This talk will summarise some of our research on how to choose predicates in a systematic way. The first part of the presentation will explain how Craig interpolation, one of the standard methods for refining abstractions, can be adapted to take program-specific information or refinement heuristics into account. The second part will present different methods to actually generate such program-specific information: with the help of upfront static analysis of a program, using domain-specific acceleration techniques, or using type-based analysis to extract variable roles.

Joint work with Yulia Demyanova, Jérôme Leroux, Pavle Subotic, and Florian Zuleger.

Bio
Philipp Ruemmer is an assistant professor at Uppsala University, Sweden. He received his doctorate in Computer Science from Chalmers University and Gothenburg University in 2008. Before joining Uppsala University as an assistant professor, he has been research assistant at the Oxford University Computing Laboratory. His research interests include various directions in program verification, theorem proving and SMT reasoning, and application of such methods in the area of embedded systems. Philipp received the Oscar Prize of Uppsala University in 2013, for contributions to the field of program correctness, and the IJCAR best paper award in 2014; the theorem prover Princess resulting from his research won the TFA division of the theorem proving competition CASC in 2012.

More information