argo-lib: A Generic Platform for Decision Procedures

1. 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)

   Chapter  Google Scholar 

2. Boyer, R.S., Moore, J.S.: Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence 11 (1988)

   Google Scholar 

3. Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. CADE-9. Springer, Heidelberg (1988)

   Google Scholar 

4. CVC Lite, on-line at: http://verify.stanford.edu/CVCL/

5. ICS, on-line at: http://www.icansolve.com/

6. Janičić, P., Bundy, A.: A General Setting for the Flexible Combining and Augmenting Decision Procedures. Journal of Automated Reasoning 28(3) (2002)

   Google Scholar 

7. Kapur, D., Subramaniam, M.: Using an induction prover for verifying arithmetic circuits. Software Tools for Technology Transfer 3(1) (2000)

   Google Scholar 

8. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2) (1979)

   Google Scholar 

9. 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)

   Google Scholar 

10. Ranise, S., Tinelli, C.: The SMT-LIB Format: An Initial Proposal (2003), on-line at: http://goedel.cs.uiowa.edu/smt-lib/

11. Rueß, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the Conference on Logic in Computer Science, LICS (2001)

    Google Scholar 

12. Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31(1) (January 1984)

    Google Scholar 

13. Stump, A., Deivanayagam, A., Kathol, S., Lingelbach, D., Schobel, D.: Rogue deicision procedures. In: Workshop PDPAR (2003)

    Google Scholar 

14. TSAT++, on-line at: http://www.mrg.dist.unige.it/Tsat

Download references