Predicate Abstraction of Programs with Non-linear Computation

Verification of programs relies on reasoning about the computations they perform. In engineering programs, many of these computations are non-linear. Although predicate abstraction enables model checking of programs with large state spaces, the decision procedures that currently support predicate abstraction are not able to handle such non-linear computations. In this paper, we propose an approach to model checking a class of data-flow properties for engineering programs that contain non-linear products and transcendental functions. The novelty of our approach is the integration of interval constraint solving techniques into the automated predicate discovery/predicate abstraction process, which extends the expressive power of predicate abstraction-based model checking. Using this approach, we construct a prototype model checker for C programs called VISA (Verification of Industrial-Strength Applications). VISA is built on top of Berkeley's BLAST and University of Nantes' Realpaver. We successfully apply VISA to scientific computation libraries and avionics applications to verify the absence of certain runtime arithmetic errors.