Advertisement

Symbolic Analysis of Transition Systems?

  • Natarajan Shankar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1912)

Abstract

We give a brief overview of the Symbolic Analysis Laboratory (SAL) project. SAL is a verification framework that is directed at analyzing properties of transition systems by combining tools for program analysis, model checking, and theorem proving. SAL is built around a small intermediate language that serves as a semantic representation for transition systems that can be used to drive the various analysis tools.

Keywords

Model Check Boolean Function Transition System Theorem Prove Reachable State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV’ 96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.zbMATHGoogle Scholar
  2. 2.
    R. Alur and T.A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7–48, 1999.CrossRefGoogle Scholar
  3. 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.MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, and implementation. Science of Computer Programming, 19(2):87–152, 1992.CrossRefzbMATHGoogle Scholar
  6. 6.
    Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Muñoz, Sam Owre, Harald Rue\, John Rushby, Vlad Rusu, Hassen Saïdi, N. Shankar, Eli Singerman, and Ashish Tiwari. An overview of SAL. In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, Hampton, VA, June 2000. NASA Langley Research Center. To appear.Google Scholar
  7. 7.
    Saddek Bensalem and Yassine Lakhnech. Automatic generation of invariants. Formal Methods in Systems Design, 15(1):75–92, July 1999.Google Scholar
  8. 8.
    Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Huand Vardi [26], pages 319–331.Google Scholar
  9. 9.
    Saddek Bensalem, Yassine Lakhnech, and Hassen6Saïdi. Powerful techniques for the automatic generation of invariants. In Alur and Henzinger [1], pages 323–335.Google Scholar
  10. 10.
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.Google Scholar
  11. 11.
    Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In E. A. Emerson and A. P. Sistla, editors, Computer-Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 2000. To appear.Google Scholar
  12. 12.
    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.CrossRefGoogle Scholar
  13. 13.
    E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999.Google Scholar
  14. 14.
    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
  15. 15.
    K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988.Google Scholar
  16. 16.
    M. A. Col on and T. E. Uribe. Generating finite-state abstractions of reactive systems using decidion procedures. In Hu and Vardi [26], pages 293–304.Google Scholar
  17. 17.
    Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Halbwachs and Peled [25], pages 160–171.Google Scholar
  18. 18.
    David L. Dill. The Murø verification system. In Alur and Henzinger [1], pages 390–393.Google Scholar
  19. 19.
    R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification,Warsaw, June 1995. North-Holland.Google Scholar
  20. 20.
    Yuri Gurevich. Evolving algebras 1993: Lipari guide. In Egon Börger, editor, Specification and Validation Methods, International Schools for Computer Scientists, pages 9–36. Oxford University Press, Oxford, UK, 1995.Google Scholar
  21. 21.
    S. M. German and B. Wegbreit. A synthesizer for inductive assertions. IEEE Transactions on Software Engineering, 1(1):68–75, March 1975.CrossRefGoogle Scholar
  22. 22.
    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
  23. 23.
    C. A. R. Hoare. An axiomatic basis of computer programming. Communications of the ACM, 12(10):576–580, October 1969.CrossRefzbMATHGoogle Scholar
  24. 24.
    G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.Google Scholar
  25. 25.
    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.zbMATHGoogle Scholar
  26. 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. 27.
    S. Katz and Z. Manna. Logical analysis of programs. Communications of the ACM, 19(4):188–206, April 1976.MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872–923, May 1994.CrossRefGoogle Scholar
  29. 29.
    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:11–44, 1995.CrossRefzbMATHGoogle Scholar
  30. 30.
    Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993.CrossRefzbMATHGoogle Scholar
  31. 31.
    Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Volume 1: Specification. Springer-Verlag, New York, NY, 1992.CrossRefzbMATHGoogle Scholar
  32. 32.
    Zohar Manna and The STeP Group. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Alur and Henzinger [1], pages 415–418.Google Scholar
  33. 33.
    A. Pnueli. The temporal logic of programs. In Proc. 18th Symposium on Foundations of Computer Science, pages 46–57, Providence, RI, November 1977. ACM.Google Scholar
  34. 34.
    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.CrossRefGoogle Scholar
  35. 35.
    Hassen Saïdi and Susanne Graf. Construction of abstract state graphs with PVS. In Orna Grumberg, editor, Computer-Aided Verification, CAV’ 97, volume 1254of Lecture Notes in Computer Science, pages 72–83, Haifa, Israel, June 1997. Springer-Verlag.CrossRefGoogle Scholar
  36. 36.
    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
  37. 37.
    Hassen Saïdi and N. Shankar. Abstract and model check while you prove. In Halbwachs and Peled [25], pages 443–454.Google Scholar
  38. 38.
    Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, pages 332–344. IEEE Computer Society Press, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Natarajan Shankar
    • 1
  1. 1.Computer Science LaboratoryUSA

Personalised recommendations