Sciweavers

Share
ATVA
2006
Springer

Predicate Abstraction of Programs with Non-linear Computation

10 years 1 months ago
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...
Songtao Xia, Ben Di Vito, César Muño
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Songtao Xia, Ben Di Vito, César Muñoz
Comments (0)
books