Solving quantified verification conditions using satisfiability modulo theories

Yeting Ge, Clark Barrett, Cesare Tinelli

Research output: Contribution to journalArticle

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 quantified benchmarks that were not solvable with previous approaches.

Original languageEnglish (US)
Pages (from-to)101-122
Number of pages22
JournalAnnals of Mathematics and Artificial Intelligence
Volume55
Issue number1-2
DOIs
StatePublished - Oct 2009

Fingerprint

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

Keywords

  • First-order logic
  • Quantified verification conditions
  • Quantifier instantiation
  • Satisfiability modulo theories

ASJC Scopus subject areas

  • Artificial Intelligence
  • Applied Mathematics

Cite this

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

In: Annals of Mathematics and Artificial Intelligence, Vol. 55, No. 1-2, 10.2009, p. 101-122.

Research output: Contribution to journalArticle

Ge, Yeting ; Barrett, Clark ; Tinelli, Cesare. / Solving quantified verification conditions using satisfiability modulo theories. In: Annals of Mathematics and Artificial Intelligence. 2009 ; Vol. 55, No. 1-2. pp. 101-122.
@article{caebeeb708f5416ab6f756bce878afe7,
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 quantified benchmarks that were not solvable with previous approaches.",
keywords = "First-order logic, Quantified verification conditions, Quantifier instantiation, Satisfiability modulo theories",
author = "Yeting Ge and Clark Barrett and Cesare Tinelli",
year = "2009",
month = "10",
doi = "10.1007/s10472-009-9153-6",
language = "English (US)",
volume = "55",
pages = "101--122",
journal = "Annals of Mathematics and Artificial Intelligence",
issn = "1012-2443",
publisher = "Springer Netherlands",
number = "1-2",

}

TY - JOUR

T1 - Solving quantified verification conditions using satisfiability modulo theories

AU - Ge, Yeting

AU - Barrett, Clark

AU - Tinelli, Cesare

PY - 2009/10

Y1 - 2009/10

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 quantified benchmarks that were not solvable with previous approaches.

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 quantified benchmarks that were not solvable with previous approaches.

KW - First-order logic

KW - Quantified verification conditions

KW - Quantifier instantiation

KW - Satisfiability modulo theories

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

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

U2 - 10.1007/s10472-009-9153-6

DO - 10.1007/s10472-009-9153-6

M3 - Article

VL - 55

SP - 101

EP - 122

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 1-2

ER -