|
 ABSTRACT
A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and ≤, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
CRAIG, W. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22 (1955).
|
 |
2
|
|
| |
3
|
|
| |
4
|
|
| |
5
|
MATIYASEVlCH, Y.V. Diophantine representation ofrecursively enumerable predicates. Proc. 2nd Scandinavian Logic Symposium, North-Holland Publ. Co., 1970.
|
| |
6
|
MCCARTHY, J. A basis for a mathematical theory of computation. In Computing Programming and Formal Systems, P. Braffort and D. Hirshberg, Eds. North-Holland Publ. Co., 1963.
|
| |
7
|
|
| |
8
|
OPPEN, D.C. Convexity, complexity, and combinations of theories. To appear in Theoretical Comptr. Sci.
|
| |
9
|
|
| |
10
|
SCHOENFIELD, J.R. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
|
| |
11
|
|
| |
12
|
SuzuKI, N., AND JEFFERSON, D. Verification decidability of Presburger array programs. Proc. Conf. on Theoretical Computer Science, U. of Waterloo, Aug. 1977.
|
| |
13
|
TAKEUC}II, I. Private communication to J. McCarthy.
|
| |
14
|
TARSKI, A. A decision method for elementary algebra and geometry. Berkeley, 1951.
|
CITED BY 88
|
|
Nevin Heintze , Joxan Jaffar , Răzvan Voicu, A framework for combining analysis and verification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-39, January 19-21, 2000, Boston, MA, USA
|
|
|
|
|
|
|
|
|
Robert B. Jones , David L. Dill , Jerry R. Burch, Efficient validity checking for processor verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.2-6, November 05-09, 1995, San Jose, California, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
D. Guaspari, Penelope, an Ada verification system, Proceedings of the conference on Tri-Ada '89: Ada technology in context: application, development, and deployment, p.216-224, January 1989, Pittsburgh, Pennsylvania, United States
|
|
|
|
|
|
|
|
|
David Y. W. Park , Jens U. Skakkebæk , Mats P. E. Heimdahl , Barbara J. Czerny , David L. Dill, Checking properties of safety critical specifications using efficient decision procedures, Proceedings of the second workshop on Formal methods in software practice, p.34-43, March 04-05, 1998, Clearwater Beach, Florida, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Eric Monfroy , Michaël Rusinowitch , René Schott, Implementing non-linear constraints with cooperative solvers, Proceedings of the 1996 ACM symposium on Applied Computing, p.63-72, February 17-19, 1996, Philadelphia, Pennsylvania, United States
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Sonia Estévez-Martín , Antonio J. Fernández , Teresa Hortalá-González , Mario Rodríguez-Artalejo , Fernando Sáenz-Pérez , Rafael del Vado Vírseda, Cooperation of constraint domains in the TOY system, Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, July 15-17, 2008, Valencia, Spain
|
|
|
|
|
|
|
|
|
D. Craigen , S. Kromodimoeljo , I. Meisels , A. Neilson , B. Pase , M. Saaltink, m-EVES: A tool for verifying software, Proceedings of the 10th international conference on Software engineering, p.324-333, April 11-15, 1988, Singapore
|
|
|
Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
|
|
|
|
|
|
|
|
|
Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi Junttila , Silvio Ranise , Peter van Rossum , Roberto Sebastiani, Efficient theory combination via boolean search, Information and Computation, v.204 n.10, p.1493-1525, October 2006
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Calogero G. Zarba , Domenico Cantone , Jacob T. Schwartz, A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case, Journal of Automated Reasoning, v.33 n.3-4, p.251-269, October 2004
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Ross Tate , Michael Stepp , Zachary Tatlock , Sorin Lerner, Equality saturation: a new approach to optimization, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
|
|
|
|
|
|
Sylvain Conchon , Evelyne Contejean , Johannes Kanig , Stéphane Lescuyer, Lightweight integration of the Ergo theorem prover inside a proof assistant, Proceedings of the second workshop on Automated formal methods, p.55-59, November 06-06, 2007, Atlanta, Georgia
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Jeremy Condit , Brian Hackett , Shuvendu K. Lahiri , Shaz Qadeer, Unifying type checking and property checking for low-level code, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
S. EstÉvez-martÍn , T. HortalÁ-gonzÁlez , M. RodrÍguez-artalejo , R. Del vado-vÍrseda , F. SÁenz-pÉrez , A. j. FernÁndez, On the cooperation of the constraint domains ℋ, ℛ, and ℱ in cflp, Theory and Practice of Logic Programming, v.9 n.4, p.415-527, July 2009
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.4