Model Checking Recursive Programs with Exact Predicate Abstraction

e Abstraction Arie Gurfinkel1 , Ou Wei2 , and Marsha Chechik2 1 Software Engineering Institute, Carnegie Mellon University 2 Department of Computer Science, University of Toronto Abstract. We propose an approach for analyzing non-termination and reachability properties of recursive programs using a combination of over- and underating abstractions. First, we define a new concrete program semantics, mixed, that combines both natural and operational semantics, and use it to design an on-the-fly symbolic algorithm. Second, we combine this algorithm with ion by following classical fixpoint abstraction techniques. This makes our approach parametrized by different approximating semantics of predicate ion and enables a uniform solution for over- and under-approximating semantics. The algorithm is implemented in YASM, and we show that it can establish non-termination of non-trivial C programs completely automatically.

• Type: Conference
• Year: 2008
• Where: ATVA
• Authors: Arie Gurfinkel, Ou Wei, Marsha Chechik
• Keywords: ATVA 2008, Carnegie Mellon University, Concrete Program Semantics, Hardware, On-the-fly Symbolic Algorithm