NDLI: Solving quantified verification conditions using satisfiability modulo theories

Content Provider	Springer Nature Link
Author	Ge, Yeting Tinelli, Cesare Barrett, Clark
Copyright Year	2009
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.
Ending Page	122
Page Count	22
Starting Page	101
File Format	PDF
ISSN	10122443
e-ISSN	15737470
Journal	Annals of Mathematics and Artificial Intelligence
Issue Number	1-2
Volume Number	55
Language	English
Publisher	Springer Netherlands
Publisher Date	2009-07-16
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	First-order logic Computer Science Artificial Intelligence (incl. Robotics) Quantified verification conditions Mathematics Satisfiability modulo theories Quantifier instantiation Theorem proving (deduction, resolution, etc.) Statistical Physics, Dynamical Systems and Complexity
Content Type	Text
Resource Type	Article
Subject	Applied Mathematics Artificial Intelligence

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A full first-order constraint solver for decomposable theories

An Instantiation Scheme for Satisfiability Modulo Theories

Inductive proof search modulo

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers

Decision procedures for extensions of the theory of arrays

Strong order equivalence

The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT

Labelled splitting

Invariants for the FoCaL language

Solving quantified verification conditions using satisfiability modulo theories

Similar Documents

A full first-order constraint solver for decomposable theories

An Instantiation Scheme for Satisfiability Modulo Theories

Inductive proof search modulo

Adding Decision Procedures to SMT Solvers Using Axioms with Triggers

Decision procedures for extensions of the theory of arrays

Strong order equivalence

The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT

Labelled splitting

Invariants for the FoCaL language

Solving quantified verification conditions using satisfiability modulo theories