Abstract
argo-lib is a C++ library that provides support for using decision procedures and for schemes for combining and augmenting decision procedures. This platform follows the smt-lib initiative which aims at establishing a library of benchmarks for satisfiability modulo theories. The platform can be easily integrated into other systems. It also enables comparison and unifying of different approaches, evaluation of new techniques and, hopefully, can help in advancing the field.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barrett, C.W., Dill, D.L., Stump, A.: A Framework for Cooperating Decision Procedures. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, Springer, Heidelberg (2000)
Boyer, R.S., Moore, J.S.: Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence 11 (1988)
Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. CADE-9. Springer, Heidelberg (1988)
CVC Lite, on-line at: http://verify.stanford.edu/CVCL/
ICS, on-line at: http://www.icansolve.com/
Janičić, P., Bundy, A.: A General Setting for the Flexible Combining and Augmenting Decision Procedures. Journal of Automated Reasoning 28(3) (2002)
Kapur, D., Subramaniam, M.: Using an induction prover for verifying arithmetic circuits. Software Tools for Technology Transfer 3(1) (2000)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2) (1979)
Ranise, S., Deharbe, D.: Light-weight theorem proving for debugging and verifying units of code. In: SEFM 2003, IEEE Computer Society Press, Los Alamitos (2003)
Ranise, S., Tinelli, C.: The SMT-LIB Format: An Initial Proposal (2003), on-line at: http://goedel.cs.uiowa.edu/smt-lib/
Rueß, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the Conference on Logic in Computer Science, LICS (2001)
Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31(1) (January 1984)
Stump, A., Deivanayagam, A., Kathol, S., Lingelbach, D., Schobel, D.: Rogue deicision procedures. In: Workshop PDPAR (2003)
TSAT++, on-line at: http://www.mrg.dist.unige.it/Tsat
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marić, F., Janičić, P. (2004). argo-lib: A Generic Platform for Decision Procedures. In: Basin, D., Rusinowitch, M. (eds) Automated Reasoning. IJCAR 2004. Lecture Notes in Computer Science(), vol 3097. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25984-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-25984-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22345-0
Online ISBN: 978-3-540-25984-8
eBook Packages: Springer Book Archive