Skip to main content
SpringerLink
Log in
Book cover

Programming Methodology pp 333–351Cite as

Automated verification using deduction, exploration, and abstraction

  • Chapter

Part of the book series: Monographs in Computer Science ((MCS))

Abstract

Computer programs are formal texts that are composed by programmers and executed by machines. Formal methods are used to predict the execution-time behavior of a program text through formal, symbolic calculation. Automation in the form of computer programs can be used to execute formal calculations so that they are reproducible and checkable. Deduction and exploration are two basic frameworks for the formal calculation of program properties. Both deduction and exploration have their limitations. We argue that these limitations can be overcome through a methodology for automated verification that uses property-preserving abstractions to bridge the gap between deduction and exploration. We introduce models, logics, and verification methods for transition systems, and outline a methodology based on the combined use of deduction, exploration, and abstraction.

This research was supported by NSF Grant CCR-0082560, DARPA/AFRL Contract F33615-00-C-3043, and NASA Contract NAS 1-00079.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   149.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104 (1): 2–34, May 1993.

    Article  MathSciNet  MATH  Google Scholar 

  2. R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems I,Lecture Notes in Computer Science 736, pages 209–229. Springer-Verlag, 1993. 16. Automated verification using deduction, exploration, and abstraction 349

    Google Scholar 

  3. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science,126(2):183–235, 25 April 1994. Fundamental Study.

    Article  MathSciNet  MATH  Google Scholar 

  4. R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In J. W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 74–106. Springer-Verlag, 1991.

    Google Scholar 

  5. Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV ‘86, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  6. 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.

    Article  MathSciNet  MATH  Google Scholar 

  7. Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Munoz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Saldi, N. Shankar, Eli Singerman, and Ashish Tiwari. An overview of SAL. In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop,pages 187–196, Hampton, VA, June 2000. NASA Langley Research Center. Proceedings available at http:// shemesh. larc.nasa.gov/fm/ Lfm2000/Proc/.

    Google Scholar 

  8. Tevfik Bultan, Richard Gerber, and William Pugh. Symbolic model checking of infinite state systems using Presburger arithmetic. In Grumberg [Gru97], pages 400–411.

    Google Scholar 

  9. R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: a system for verification and synthesis. In Alur and Henzinger [AH96], pages 428–432.

    Google Scholar 

  10. Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Hu and Vardi [HV98], pages 319–331.

    Google Scholar 

  11. K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package. In Proc. of the 27th ACM/IEEE Design Automation Conference, pages 40–45, 1990.

    Chapter  Google Scholar 

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

    Google Scholar 

  13. James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering,pages 439–448, Limerick, Ireland, June 2000. IEEE Computer Society.

    Google Scholar 

  14. E.M. Clark, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16 (5): 1512–1542, September 1994.

    Article  Google Scholar 

  15. E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999. 350 Shankar

    Google Scholar 

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

    MATH  Google Scholar 

  17. M. A. Colón and T. E. Uribe. Generating finite-state abstractions of reactive systems using decidion procedures. In Hu and Vardi [HV98], pages 293–304.

    Google Scholar 

  18. Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Halbwachs and Peled [HP99], pages 160–171.

    Google Scholar 

  19. David L. Dill. The Mur0 verification system. In Alur and Henzinger [AH96], pages 390–393.

    Google Scholar 

  20. Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors. Compositionality: The Significant Difference (Revised lectures from International Symposium COMPOS’97), volume 1536 of Lecture Notes in Computer Science, Bad Malente, Germany, September 1997. Springer-Verlag.

    Google Scholar 

  21. E. Allen Emerson and Joseph Y. Halpern. “sometimes” and “not never” revisited: On branching versus linear time. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, pages 127–140, Austin, Texas, January 1983.

    Google Scholar 

  22. E. Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 16, pages 995–1072. Elsevier and MIT press, Amsterdam, The Netherlands, and Cambridge, MA, 1990.

    Google Scholar 

  23. Formal Systems (Europe) Ltd, Oxford, UK. Failures Divergence Refinement: User Manual and Tutorial, 1.20 edition, October 1992.

    Google Scholar 

  24. Orna Grumberg, editor. Computer-Aided Verification, CAV ‘87, volume 1254 of Lecture Notes in Computer Science, Haifa, Israel, June 1997. Springer-Verlag.

    Google Scholar 

  25. C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(101: 576–583, 1969.

    Google Scholar 

  26. C. A. R. Hoare. Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, 1985.

    MATH  Google Scholar 

  27. G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  30. R.P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1993.

    Google Scholar 

  31. Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16 (3): 872–923, May 1994.

    Article  Google Scholar 

  32. N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Annual Symposium on Principles of Distributed Computing,pages 137–151, New York, 1987. ACM Press. 16. Automated verification using deduction, exploration, and abstraction 351

    Google Scholar 

  33. K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993.

    Book  MATH  Google Scholar 

  34. R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

    MATH  Google Scholar 

  35. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer-Verlag, New York, NY, 1992.

    Book  Google Scholar 

  36. K. McMillan, S. Qadeer, and J. Saxe. Induction in compositional model checking. In E. A. Emerson and A. P. Sistla, editors, Computer-Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 312–327, Chicago, IL, July 2000. Springer-Verlag. [ORSvH95] S. Owre, J. Rushby, N. Shankar, and E. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  38. S. Rajan, N. Shankar, and M. Srivas. An integration of theorem proving and automated proof checking. In Computer-Aided Verification, number 939 in Lecture Notes in Computer Science, pages 84–97. Springer-Verlag, 1995.

    Google Scholar 

  39. D. Scott and J. W. de Bakker. A theory of programs, unpublished notes. IBM Seminar, Vienna, 1969.

    Google Scholar 

  40. SG97] Hassen Saldi and Susanne Graf. Construction of abstract state graphs with PVS. In Grumberg [Gru97], pages 72–83.

    Google Scholar 

  41. 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 

  42. Hassen Saldi and N. Shankar. Abstract and model check while you prove. In Halbwachs and Peled [HP99], pages 443–454.

    Google Scholar 

  43. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. of Math., 5: 285–309, 1955.

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SRI International Computer Science Laboratory, Menlo Park, CA, 94025, USA

    Natarajan Shankar

Authors
  1. Natarajan Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Macquarie University, 2109, Sydney, Australia

    Annabelle McIver

  2. Department of Computer Science and Engineering, The University of New South Wales, 2052, Sydney, Australia

    Carroll Morgan

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer Science+Business Media New York

About this chapter

Cite this chapter

Shankar, N. (2003). Automated verification using deduction, exploration, and abstraction. In: McIver, A., Morgan, C. (eds) Programming Methodology. Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-0-387-21798-7_16

Download citation

  • DOI: https://doi.org/10.1007/978-0-387-21798-7_16

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4419-2964-8

  • Online ISBN: 978-0-387-21798-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation