Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems

Sicun Gao, Malay Ganai, Franjo Ivančić, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

26 Scopus citations

Abstract

We propose a novel integration of interval constraint propagation (ICP) with SMT solvers for linear real arithmetic (LRA) to decide nonlinear real arithmetic problems. We use ICP to search for interval solutions of the nonlinear constraints, and use the LRA solver to either validate the solutions or provide constraints to incrementally refine the search space for ICP. This serves the goal of separating the linear and nonlinear solving stages, and we show that the proposed methods preserve the correctness guarantees of ICP. Experimental results show that such separation is useful for enhancing efficiency.

Original languageEnglish (US)
Title of host publicationFormal Methods in Computer Aided Design, FMCAD 2010
Pages81-89
Number of pages9
StatePublished - Dec 1 2010
Externally publishedYes
EventFormal Methods in Computer Aided Design, FMCAD 2010 - Lugano, Switzerland
Duration: Oct 20 2010Oct 23 2010

Publication series

NameFormal Methods in Computer Aided Design, FMCAD 2010

Other

OtherFormal Methods in Computer Aided Design, FMCAD 2010
CountrySwitzerland
CityLugano
Period10/20/1010/23/10

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems'. Together they form a unique fingerprint.

  • Cite this

    Gao, S., Ganai, M., Ivančić, F., Gupta, A., Sankaranarayanan, S., & Clarke, E. M. (2010). Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In Formal Methods in Computer Aided Design, FMCAD 2010 (pp. 81-89). [5770936] (Formal Methods in Computer Aided Design, FMCAD 2010).