Sciweavers

Share
ATVA
2008
Springer

Model Checking Recursive Programs with Exact Predicate Abstraction

11 years 1 months ago
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.
Arie Gurfinkel, Ou Wei, Marsha Chechik
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ATVA
Authors Arie Gurfinkel, Ou Wei, Marsha Chechik
Comments (0)
books