Solving quantified verification conditions using satisfiability modulo theories

Yeting Ge, Clark Barrett, Cesare Tinelli

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

Abstract

First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics. Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, this paper describes a methodology for reasoning about quantifiers in SMT systems. We present the methodology in the context of the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify's techniques, we also introduce a number of new heuristics. Most important is the notion of instantiation level which provides an effective mechanism for prioritizing and managing the large search space inherent in quantifier instantiation techniques. These techniques have been implemented in the SMT system CVC3. Experimental results show that our methodology enables CVC3 to solve a significant number of benchmarks that were not solvable with any previous approach.

Original languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
Pages167-182
Number of pages16
Volume4603 LNAI
StatePublished - 2007
Event21st International Conference on Automated Deduction, CADE-21 2007 - Bremen, Germany
Duration: Jul 17 2007Jul 20 2007

Other

Other21st International Conference on Automated Deduction, CADE-21 2007
CountryGermany
CityBremen
Period7/17/077/20/07

Fingerprint

Theorem proving
Systems Theory
Automated Theorem Proving
Quantifiers
Modulo
System theory
Simplify
Reasoning
Benchmarking
Methodology
Legacy systems
Heuristics
Legacy Systems
First-order Logic
Search Space
Benchmark
First-order
Alternatives
Experimental Results

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Ge, Y., Barrett, C., & Tinelli, C. (2007). Solving quantified verification conditions using satisfiability modulo theories. In Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings (Vol. 4603 LNAI, pp. 167-182)

Solving quantified verification conditions using satisfiability modulo theories. / Ge, Yeting; Barrett, Clark; Tinelli, Cesare.

Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Vol. 4603 LNAI 2007. p. 167-182.

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

Ge, Y, Barrett, C & Tinelli, C 2007, Solving quantified verification conditions using satisfiability modulo theories. in Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. vol. 4603 LNAI, pp. 167-182, 21st International Conference on Automated Deduction, CADE-21 2007, Bremen, Germany, 7/17/07.
Ge Y, Barrett C, Tinelli C. Solving quantified verification conditions using satisfiability modulo theories. In Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Vol. 4603 LNAI. 2007. p. 167-182
Ge, Yeting ; Barrett, Clark ; Tinelli, Cesare. / Solving quantified verification conditions using satisfiability modulo theories. Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Vol. 4603 LNAI 2007. pp. 167-182
@inproceedings{61cfce3a8faf4fc6ba20b60b4dcd85b7,
title = "Solving quantified verification conditions using satisfiability modulo theories",
abstract = "First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics. Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, this paper describes a methodology for reasoning about quantifiers in SMT systems. We present the methodology in the context of the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify's techniques, we also introduce a number of new heuristics. Most important is the notion of instantiation level which provides an effective mechanism for prioritizing and managing the large search space inherent in quantifier instantiation techniques. These techniques have been implemented in the SMT system CVC3. Experimental results show that our methodology enables CVC3 to solve a significant number of benchmarks that were not solvable with any previous approach.",
author = "Yeting Ge and Clark Barrett and Cesare Tinelli",
year = "2007",
language = "English (US)",
isbn = "3540735941",
volume = "4603 LNAI",
pages = "167--182",
booktitle = "Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings",

}

TY - GEN

T1 - Solving quantified verification conditions using satisfiability modulo theories

AU - Ge, Yeting

AU - Barrett, Clark

AU - Tinelli, Cesare

PY - 2007

Y1 - 2007

N2 - First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics. Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, this paper describes a methodology for reasoning about quantifiers in SMT systems. We present the methodology in the context of the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify's techniques, we also introduce a number of new heuristics. Most important is the notion of instantiation level which provides an effective mechanism for prioritizing and managing the large search space inherent in quantifier instantiation techniques. These techniques have been implemented in the SMT system CVC3. Experimental results show that our methodology enables CVC3 to solve a significant number of benchmarks that were not solvable with any previous approach.

AB - First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first order automated theorem proving (ATP) and automated theorem proving based on satisfiability modulo theories (SMT). Traditional ATP systems are designed to handle quantifiers easily, but often have difficulty reasoning with respect to theories. SMT systems, on the other hand, have built-in support for many useful theories, but have a much more difficult time with quantifiers. One clue on how to get the best of both worlds can be found in the legacy system Simplify which combines built-in theory reasoning with quantifier instantiation heuristics. Inspired by Simplify and motivated by a desire to provide a competitive alternative to ATP systems, this paper describes a methodology for reasoning about quantifiers in SMT systems. We present the methodology in the context of the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify's techniques, we also introduce a number of new heuristics. Most important is the notion of instantiation level which provides an effective mechanism for prioritizing and managing the large search space inherent in quantifier instantiation techniques. These techniques have been implemented in the SMT system CVC3. Experimental results show that our methodology enables CVC3 to solve a significant number of benchmarks that were not solvable with any previous approach.

UR - http://www.scopus.com/inward/record.url?scp=35148866683&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35148866683&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:35148866683

SN - 3540735941

SN - 9783540735946

VL - 4603 LNAI

SP - 167

EP - 182

BT - Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings

ER -