Predicate Abstraction of Programs with Non-linear Computation

e Abstraction of Programs With Non-linear Computation Songtao Xia1 Ben Di Vito2 Cesar Munoz3 1 NASA Postdoc at NASA Langley Research Center, Hampton, VA 2 NASA Langley Research Center, Hampton, VA 3 National Institute of Aerospace, Hampton, VA Abstract. Verification of programs relies on reasoning about the computations they perform. In engineering programs, many of these coms 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 nonlinear 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 automated predicate discovery/predicate abstraction process, tends the expressive power of predicate abstraction-based model ch...

• Type: Conference
• Year: 2006
• Where: ATVA
• Authors: Songtao Xia, Ben Di Vito, César Muñoz
• Keywords: ATVA 2006, Hardware, Model Checking, NASA Langley Research Center, Predicate Abstraction