A rewriting approach to satisfiability procedures, Information and Computation, vol.183, issue.2, pp.140-164, 2003. ,
DOI : 10.1016/S0890-5401(03)00020-8
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic, Proceedings of TACAS'03, 2003. ,
DOI : 10.1007/3-540-36577-X_38
Integrating Decision Procedures for Temporal Verification, 1998. ,
Justifying Equality, PDPAR, 2004. ,
DOI : 10.1016/j.entcs.2004.06.068
Light-weight theorem proving for debugging and verifying units of code, First International Conference onSoftware Engineering and Formal Methods, 2003.Proceedings., 2003. ,
DOI : 10.1109/SEFM.2003.1236224
ICS: Integrated Canonizer and Solver?, Computer Aided Verification (CAV), volume 2102 of LNCS, pp.246-249, 2001. ,
DOI : 10.1007/3-540-44585-4_22
Combining Non-stably Infinite, Non-first Order Theories, Pragmatics of Decision Procedures in Automated Reasoning, 2004. ,
DOI : 10.1016/j.entcs.2004.06.066
Automated Deduction ? CADE-18, LNCS, vol.2392, pp.332-346, 2002. ,
Reasoning about Numbers in Tecton, Proc. 8 th Inl. Symp. Methodologies for Intelligent Systems, pp.57-70, 1994. ,
Automating Recursive Type Definitions in Higher Order Logic, Current Trends in Hardware Verification and Theorem Proving, pp.341-386, 1989. ,
DOI : 10.1007/978-1-4612-3658-0_9
Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980. ,
DOI : 10.1145/322186.322198
Reasoning About Recursively Defined Data Structures, Journal of the ACM, vol.27, issue.3, pp.403-411, 1980. ,
DOI : 10.1145/322203.322204
Abstract Datatypes in PVS, 1997. ,
A fixedpoint approach to implementing (Co)inductive definitions, Automated Deduction ? CADE-12, LNAI 814, pp.148-161 ,
DOI : 10.1007/3-540-58156-1_11
The omega test: a fast integer programming algorithm for dependence analysis. Supercomputing, pp.4-13, 1991. ,
Deciding Combinations of Theories, Journal of the ACM, vol.31, issue.1, pp.1-12, 1984. ,
DOI : 10.1145/2422.322411
CVC: A Cooperating Validity Checker, Computer Aided Verification (CAV), pp.500-504, 2002. ,
DOI : 10.1007/3-540-45657-0_40
Combining Non-Stably Infinite Theories, Electronic Notes in Theoretical Computer Science, vol.86, issue.1, 2004. ,
DOI : 10.1016/S1571-0661(04)80651-0
On the Construction of Automata from Linear Arithmetic Constraints, TACAS, pp.1-19, 2000. ,
DOI : 10.1007/3-540-46419-0_1
Combining Multisets with Integers, Automated Deduction ? CADE-18, pp.363-376, 2002. ,
DOI : 10.1007/3-540-45620-1_30
Combining Sets with Integers, Frontiers of Combining Systems, pp.103-116, 2002. ,
DOI : 10.1007/3-540-45988-X_9
Combining Sets with Elements, Theory and Practice, pp.762-782, 2004. ,
DOI : 10.1007/978-3-540-39910-0_33
Decision Procedures for Recursive Data Structures with Integer Constraints, Automated Reasoning, pp.152-167, 2004. ,
DOI : 10.1007/978-3-540-25984-8_9