Combining Theorem Proving and Model Checking through Symbolic Analysis

1. Rajeev Alur and Thomas A. Henzinger. Reactive modules. In Proceedings, 11 ^th Annual IEEE Symposium on Logic in Computer Science, pages 207–218, New Brunswick, New Jersey, 27–30 July 1996. IEEE Computer Society Press.

   Google Scholar 

2. Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, and Joseph Sifakis. Property preserving simulations. In Computer-Aided Verification, CAV’ 92, volume 630 of Lecture Notes in Computer Science, pages 260–273, Montréal, Canada, June 1992. Springer-Verlag. Extended version available with title “Property Preserving Abstractions.”.

   Google Scholar 

3. Nikolaj Bjørner, I. Anca Browne, and Zohar Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49–87, 1997.

   Article  MATH  MathSciNet  Google Scholar 

4. BCM⁺92._J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10²⁰ states and beyond. Information and Computation, 98(2):142–170, June 1992.

   Google Scholar 

5. Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD’ 96), volume 1166 of Lecture Notes in Computer Science, pages 187–201, Palo Alto, CA, November 1996. Springer-Verlag.

   Chapter  Google Scholar 

6. G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, and implementation. Science of Computer Programming, 19(2):87–152, 1992.

   Article  MATH  Google Scholar 

7. Saddek Bensalem and Yassine Lakhnech. Automatic generation of invariants. Formal Methods in Systems Design, 15(1):75–92, July 1999.

   Google Scholar 

8. Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98], pages 319–331.

   Chapter  Google Scholar 

9. Saddek Bensalem, Yassine Lakhnech, and Hassen Saïdi. Powerful techniques for the automatic generation of invariants. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, pages 323–335, New Brunswick, NJ, July/August 1996. Springer-Verlag.

   Google Scholar 

10. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis. In 4th ACM Symposium on Principles of Programming Languages. Association for Computing Machinery, January 1977.

    Google Scholar 

11. Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, September 1994.

    Google Scholar 

12. E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999.

    Google Scholar 

13. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables. In 5th ACM Symposium on Principles of Programming Languages. Association for Computing Machinery, January 1978.

    Google Scholar 

14. K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.

    MATH  Google Scholar 

15. M. A. Colon and T. E. Uribe. Generating finite-state abstractions of reactive systems using decidion procedures. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98], pages 293–304.

    Chapter  Google Scholar 

16. Dennis René Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The Netherlands, July 1996.

    MATH  Google Scholar 

17. Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Doron Peled, editors. Computer-Aided Verification, CAV’ 99, volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag Halbwachs and Peled [HP99], pages 160–171.

    Chapter  Google Scholar 

18. David L. Detlefs. An overview of the Extended Static Checking system. In First Workshop on Formal Methods in Software Practice (FMSP’ 96), pages 1–9, San Diego, CA, January 1996. Association for Computing Machinery.

    Google Scholar 

19. Jürgen Dingel and Thomas Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Computer-Aided Verification 95, 1995. This volume.

    Google Scholar 

20. Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, ∃CTL* and CTL*. In Ernst-Rüdiger Olderog, editor, Programming Concepts, Methods and Calculi (PROCOMET’ 94), pages 561–581, 1994.

    Google Scholar 

21. M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK, 1993.

    MATH  Google Scholar 

22. S. M. German and B. Wegbreit. A synthesizer for inductive assertions. IEEE Transactions on Software Engineering, 1(1):68–75, March 1975.

    Google Scholar 

23. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305–1320, September 1991.

    Google Scholar 

24. Nicolas Halbwachs and Doron Peled, editors. Computer-Aided Verification, CAV’ 99, volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.

    Google Scholar 

25. L. Helmink, M. P. A. Sellink, and F. W. Vaandrager. Proof-checking a data link protocol. Technical Report CS-R9420, Centrum voor Wiskunde en Informatica (CWI), Amsterdam, The Netherlands, March 1994.

    Google Scholar 

26. Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV’ 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag.

    Google Scholar 

27. G. Janssen. ROBDD Software Department of Electrical Engineering, Eindhoven University of Technology, October 1993.

    Google Scholar 

28. Jeffrey J. Joyce and Carl-Johan H. Seger. Linking BDD-based symbolic evaluation to interactive theorem proving. In Proceedings of the 30th Design Automation Conference. Association for Computing Machinery, 1993.

    Google Scholar 

29. S. Katz and Z. Manna. Logical analysis of programs. Communications of the ACM, 19(4):188–206, 1976.

    Article  MATH  MathSciNet  Google Scholar 

30. R. P. Kurshan. Computer-Aided Verification of Coordinating Processes— The Automata-Theoretic Approach. Princeton University Press, Princeton, NJ, 1994.

    Google Scholar 

31. Leslie Lamport. A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM, 17(8):453–455, August 1974.

    Google Scholar 

32. LGS⁺95._C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1–44, 1995.

    Article  Google Scholar 

33. Zohar Manna, Anca Browne, Henny B. Sipma, and Tomás E. Uribe. Visual abstractions for temporal verification. In Armando M. Haeberer, editor, Algebraic Methodology and Software Technology, AMAST’98, volume 1548 of Lecture Notes in Computer Science, pages 28–41, Amazonia, Brazil, January 1999. Springer-Verlag.

    Chapter  Google Scholar 

34. Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993.

    MATH  Google Scholar 

35. K. L. McMillan. Verification of infinite state systems by compositional model checking. In Laurence Pierre and Thomas Kropf, editors, Correct Hardware Design and Verification Methods, number 1703 in Lecture Notes in Computer Science, pages 219–233. Springer Verlag, September 1999.

    Google Scholar 

36. Ralph Melton and David L. Dill. Murφ Annotated Reference Manual. Computer Science Department, Stanford University, Stanford, CA, March 1993.

    Google Scholar 

37. K. McMillan, S. Qadeer, and J. Saxe. Induction in compositional model checking. In E. A. Emerson and A. P. Sistla, editors, Computer-Aided Verification, Lecture Notes in Computer Science. Springer Verlag, 2000. To appear.

    Google Scholar 

38. Z. Manna and the STeP Group. STeP: The Stanford Temporal Prover. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors, TAPSOFT’ 95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 793–794, Aarhus, Denmark, May 1995. Springer Verlag.

    Google Scholar 

39. Sam Owre, John M. Rushby, and Natarajan Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, Automated Deduction-CADE-11, 11th International Conference on Automated Deduction, Lecture Notes in Artifical Intelligence, pages 748–752. Springer Verlag, June 1992.

    Google Scholar 

40. David Park. Finiteness is mu-ineffable. Theoretical Computer Science, 3:173–181, 1976.

    Article  MathSciNet  Google Scholar 

41. H. Rueß and N. Shankar. Deconstructing Shostak. Available from http://www.csl.sri.com/shankar/shostak2000.ps.gz., January 2000.

42. S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV’ 95, volume 939 of Lecture Notes in Computer Science, pages 84–97, Liege, Belgium, June 1995. Springer-Verlag.

    Google Scholar 

43. Hassen Saïdi. A tool for proving invariance properties of concurrent systems automatically. In Tools and Algorithms for the Construction and Analysis of Systems TACAS’ 96, volume 1055 of Lecture Notes in Computer Science, pages 412–416, Passau, Germany, March 1996. Springer-Verlag.

    Google Scholar 

44. Carl-Johan H. Seger. Formal methods in CAD from an industrial perspective. In Ganesh Gopalakrishnan and Phillip Windley, editors, Formal Methods in Computer-Aided Design (FMCAD’ 98), volume 1522 of Lecture Notes in Computer Science, Palo Alto, CA, November 1998. Springer-Verlag.

    Chapter  Google Scholar 

45. Hassen Saïdi and Susanne Graf. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer-Aided Verification, CAV’ 97, volume 1254 of Lecture Notes in Computer Science, pages 72–83, Haifa, Israel, June 1997. Springer-Verlag.

    Google Scholar 

46. N. Shankar. Machine-assisted verification using theorem proving and model checking. In M. Broy and Birgit Schieder, editors, Mathematical Methods in Program Development, volume 158 of NATO ASI Series F: Computer and Systems Science, pages 499–528. Springer, 1997.

    Google Scholar 

47. N. Suzuki and K. Ishihata. Implementation of an array bound checker. In 4th ACM Symposium on Principles of Programming Languages, pages 132–143, January 1977.

    Google Scholar 

48. Hassen Saïdi and N. Shankar. Abstract and model check while you prove. In Doron Peled, editors. Computer-Aided Verification, CAV’ 99, volume 1633 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag Halbwachs and Peled [HP99], pages 443–454.

    Chapter  Google Scholar 

Download references