A Framework for Cooperating Decision Procedures

1. Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson–Oppen combination method. In: McCune, W. (ed.) 14th International Conference on Computer Aided Deduction. LNCS, pp. 19–33. Springer, Heidelberg (1997)

   Google Scholar 

2. Barrett, C., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)

   Chapter  Google Scholar 

3. Bjorner, N.: Integrating Decision Procedures for Temporal Verification. PhD thesis. Stanford University (1999)

   Google Scholar 

4. Colon, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 293–304. Springer, Heidelberg (1998)

   Chapter  Google Scholar 

5. Cyrluk, D.: Private communication (1999)

   Google Scholar 

6. Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak’s Decision Procedure for Com- binations of Theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 463–477. Springer, Heidelberg (1996)

   Google Scholar 

7. Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: 11th International Conference on Computer-Aided Verification, Trento, Italy, pp. 160–172. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

8. Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, Compaq SRC (1998)

   Google Scholar 

9. Manna, Z., et al.: STeP: Deductive-Algorithmic Verification of Reactive and Real- time Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 415–418. Springer, Heidelberg (1996)

   Google Scholar 

10. Saidi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

11. Levitt, J.: Formal Verification Techniques for Digital Systems. PhD thesis. Stanford University (1999)

    Google Scholar 

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

    Article  MATH  Google Scholar 

13. Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

14. Park, D.Y.W., Skakkebæk, J.U., Heimdahl, M.P.E., Czerny, B.J., Dill, D.L.: Checking properties of safety critical specifications using efficient decision procedures. In: FMSP 1998: Second Workshop on Formal Methods in Software Practice, March 1998, pp. 34–43 (1998)

    Google Scholar 

15. Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM 8, 102–114 (1992)

    Article  Google Scholar 

16. Ruess, H., Shankar, N.: Deconstructing Shostak. In: 17th International Conference on Computer Aided Deduction (2000)

    Google Scholar 

17. Shostak, R.: Deciding combinations of theories. Journal of the Association for Computing Machinery 31(1), 1–12 (1984)

    MATH  MathSciNet  Google Scholar 

18. Su, J., Dill, D., Skakkebæk, J.: Formally verifying data and control with weak reachability invariants. Formal Method In Computer-Aided Design (1998)

    Google Scholar 

19. Tinelli, C., Harandi, M.: A new Correctness Proof of the Nelson–Oppen Combination Procedure. In: Baader, F., Schulz, K. (eds.) 1st International Workshop on Frontiers of Combining Systems (FroCoS’96). Applied Logic Series, vol. 3. Kluwer Academic Publishers, Dordrecht (1996)

    Google Scholar 

Download references