Abstract
Introduction
Chapter PDF
References
Barrett, C., de Moura, L., Stump, A.: Smt-comp: Satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20–23. Springer, Heidelberg (2005)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: The mathSAT 3 system. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 315–321. Springer, Heidelberg (2005)
de Moura, L.: System description: Yices 0.1. Technical report, Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94062 (July 2005), http://fm.csl.sri.com/yices
Dutertre, B., de Moura, L.: Simplics: Tool description. Technical report, Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94062 (July 2005), http://fm.csl.sri.com/simplics
Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 246. Springer, Heidelberg (2001)
Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005)
Ramani, A., Aloul, F.A., Markov, I.L., Sakallah, K.A.: Dynamic symmetry-breaking for improved boolean optimization. In: Asia and South Pacific Design Automation Conference (ASP-DAC) (Januray 2005)
Ranise, S., Tinelli, C.: The smt-lib standard: Version 1.1. Technical report, Department of Computer Science, The University of Iowa (2005), Available at: goedel.cs.uiowa.edu/smtlib
Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid sat-based decision procedure for separation logic with uninterpreted functions. In: Proc. 40th Design Automation Conference (DAC), pp. 425–430 (June 2003)
Strichman, O., Seshia, S., Bryant, R.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 209. Springer, Heidelberg (2002)
Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 500. Springer, Heidelberg (2002)
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roe, K. (2006). The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_42
Download citation
DOI: https://doi.org/10.1007/11817963_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)