Deciding Combinations of Theories

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Deciding Combinations of Theories

Full text

Pdf (582 KB)

Source

Journal of the ACM (JACM) archive
Volume 31 , Issue 1 (January 1984) table of contents

Pages: 1 - 12

Year of Publication: 1984

ISSN:0004-5411

Author

Robert E. Shostak

Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 54, Citation Count: 28

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/2422.322411 What is a DOI?

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	Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
	2	David Randolph Jefferson, Type reduction and program verification, 1980
	3	MELL/AR-SMITH, P.M., AND SCHWARTZ, R.L.Formal specification and mechanical verificatton of SIFT. A fault-tolerant flight control system. IEEE Trans Comput 31, 7 (July 1982), 616--630.
	4	Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
	5	Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
	6	Robert E. Shostak, An algorithm for reasoning about equality, Communications of the ACM, v.21 n.7, p.583-585, July 1978 [doi>10.1145/359545.359570]
	7	Robert E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM (JACM), v.26 n.2, p.351-360, April 1979 [doi>10.1145/322123.322137]
	8	Robert E. Shostak , Richard L. Schwartz , P. M. Melliar-Smith, STP: A Mechanized Logic for Specification and Verification, Proceedings of the 6th Conference on Automated Deduction, p.32-49, June 07-09, 1982
	9	Robert Endre Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM (JACM), v.22 n.2, p.215-225, April 1975 [doi>10.1145/321879.321884]
	10	WeNSLEV, J., et alL, SIFT. Design and analysis of a fault-tolerant computer for aircraft control. Proc IEEE 66, 10 (Oct. 1978)

CITED BY 28

	Alessandro Armando , Silvio Ranise, Constraint contextual rewriting, Journal of Symbolic Computation, v.36 n.1-2, p.193-216, July 2003
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	Allen Goldberg , T. C. Wang , David Zimmerman, Applications of feasible path analysis to program testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.80-94, August 17-19, 1994, Seattle, Washington, United States
	Cesare Tinelli , Christophe Ringeissen, Unions of non-disjoint theories and combinations of satisfiability procedures, Theoretical Computer Science, v.290 n.1, p.291-353, 1 January 2003
	Sumit Gulwani , George C. Necula, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols, Information and Computation, v.199 n.1-2, p.107-131, 25 May 2005
	Alessandro Armando , Silvio Ranise , Michaël Rusinowitch, A rewriting approach to satisfiability procedures, Information and Computation, v.183 n.2, p.140-164, 15 June 2003
	John Rushby, Theorem proving for verification, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Guillem Godoy , Robert Nieuwenhuis , Ashish Tiwari, Classes of term rewrite systems with polynomial confluence problems, ACM Transactions on Computational Logic (TOCL), v.5 n.2, p.321-331, April 2004
	Rakesh Verma, Algorithms and reductions for rewriting problems. II, Information Processing Letters, v.84 n.4, p.227-233, 30 November 2002
	Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995
	David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005
	Eyal Amir , Sheila McIlraith, Partition-based logical reasoning for first-order and propositional theories, Artificial Intelligence, v.162 n.1-2, p.49-88, February 2005
	Sava Krstić , Sylvain Conchon, Canonization for disjoint unions of theories, Information and Computation, v.199 n.1-2, p.87-106, 25 May 2005
	Sylvain Conchon , Sava Krstić, Strategies for combining decision procedures, Theoretical Computer Science, v.354 n.2, p.187-210, 28 March 2006
	Leo Bachmair , Ashish Tiwari , Laurent Vigneron, Abstract Congruence Closure, Journal of Automated Reasoning, v.31 n.2, p.129-168, 2003
	David Currie , Xiushan Feng , Masahiro Fujita , Alan J. Hu , Mark Kwan , Sreeranga Rajan, Embedded software verification using symbolic execution and uninterpreted functions, International Journal of Parallel Programming, v.34 n.1, p.61-91, Febraury 2006
	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
	Lucas Bordeaux , Youssef Hamadi , Lintao Zhang, Propositional Satisfiability and Constraint Programming: A comparative survey, ACM Computing Surveys (CSUR), v.38 n.4, p.12-es, 2006
	Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine, Combining Decision Procedures by (Model-)Equality Propagation, Electronic Notes in Theoretical Computer Science (ENTCS), 240, p.113-128, July, 2009
	Nikolaj S. Bjørner , Anca Browne , Michael A. Colón , Bernd Finkbeiner , Zohar Manna , Henny B. Sipma , Tomás E. Uribe, Verifying Temporal Properties of Reactive Systems: A STeP Tutorial, Formal Methods in System Design, v.16 n.3, p.227-270, June 2000
	Ajay Chander , David Espinosa , Nayeem Islam , Peter Lee , George C. Necula, Enforcing resource bounds via static verification of dynamic checks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.5, p.28-es, August 2007
	Leonardo de Moura , Nikolaj Bjørner, Model-based Theory Combination, Electronic Notes in Theoretical Computer Science (ENTCS), v.198 n.2, p.37-49, May, 2008
	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
	Sylvain Conchon , Jean-Christophe Filliâtre, A persistent union-find data structure, Proceedings of the 2007 workshop on Workshop on ML, October 05-05, 2007, Freiburg, Germany
	Sylvain Conchon , Evelyne Contejean , Johannes Kanig , Stéphane Lescuyer, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Electronic Notes in Theoretical Computer Science (ENTCS), v.198 n.2, p.51-69, May, 2008
	Alessandro Armando , Maria Paola Bonacina , Silvio Ranise , Stephan Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic (TOCL), v.10 n.1, p.1-51, January 2009
	Mark E. Stickel, Automated deduction by theory resolution, Proceedings of the 9th international joint conference on Artificial intelligence, p.1181-1186, August 18-23, 1985, Los Angeles, California
	Andrei Voronkov, Automated reasoning: past story and new trends, Proceedings of the 18th international joint conference on Artificial intelligence, p.1607-1612, August 09-15, 2003, Acapulco, Mexico