Advertisement

Computer-aided computing

  • Natarajan Shankar
Invited Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)

Abstract

Formal program design methods are most useful when supported with suitable mechanization. This need for mechanization has long been apparent, but there have been doubts whether verification technology could cope with the problems of scale and complexity. Though there is very little compelling evidence either way at this point, several powerful mechanical verification systems are now available for experimentation. Using SRI's PVS as one representative example, we argue that the technology of mechanical verification is already quite effective. PVS derives its power from an integration of theorem proving with type-checking, decision procedures with interactive proof construction, and more recently, model checking with theorem proving. We discuss these individual aspects of PVS using examples, and motivate some of the challenges that lie ahead.

Keywords

Model Check Decision Procedure Critical Section Mutual Exclusion Proof Obligation 
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.
    William R. Bevier, Warren A. Hunt, Jr., J Strother Moore, and William D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428, December 1989.Google Scholar
  2. 2.
    R. S. Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, New York, NY, 1988.Google Scholar
  3. 3.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In 5th Annual IEEE Symposium on Logic in Computer Science, pages 428–439, Philadelphia, PA, June 1990. IEEE Computer Society.Google 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.Google Scholar
  5. 5.
    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
  6. 6.
    R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.Google Scholar
  7. 7.
    T. Coquand and G. P. Huet. Constructions: A higher order proof system for mechanizing mathematics. In Proceedings of EUROCAL 85, Linz (Austria), Berlin, 1985. Springer-Verlag.Google Scholar
  8. 8.
    Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, and Mark Saaltink. EVES: An overview. In S. Prehn and W. J. Toetenel, editors, VDM '91: Formal Software Development Methods, volume 551 of Lecture Notes in Computer Science, pages 389–405, Noordwijkerhout, The Netherlands, October 1991. Springer-Verlag. Volume 1: Conference Contributions.Google Scholar
  9. 9.
    D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Preliminary Proceedings of the Second Conference on Theorem Provers in Circuit Design, pages 287–305, Bad Herrenalb (Blackforest), Germany, September 1994. Forschungszentrum Informatik an der Universität Karlsruhe, FZI Publication 4/94.Google Scholar
  10. 10.
    David Cyrluk, Patrick Lincoln, Paliath Narendran, Sam Owre, Sreeranga Ragan, John Rushby, Natarajan Shankar, Jens Ulrik Skakkebæk, Mandayam Srivas, and Friedrich von Henke. Seven papers on mechanized formal verification. Technical Report SRI-CSL-95-3, Computer Science Laboratory, SRI International, Menlo Park, CA, January 1995.Google Scholar
  11. 11.
    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
  12. 12.
    Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271–280, May 1979.Google Scholar
  13. 13.
    E.A. Emerson and C.L Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the 10th Symposium on Principles of Programming Languages, pages 84–96, New Orleans, LA, January 1985. Association for Computing Machinery.Google Scholar
  14. 14.
    William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11(2):213–248, October 1993.Google Scholar
  15. 15.
    Stephen J. Garland and John V. Guttag. LP: The Larch prover. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction (CADE), volume 310 of Lecture Notes in Computer Science, pages 748–749, Argonne, IL, May 1988. Springer-Verlag.Google Scholar
  16. 16.
    M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.Google Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    Constance Heitmeyer and Nancy Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. In Real Time Systems Symposium, pages 120–131, San Juan, Puerto Rico, December 1994. IEEE Computer Society.Google Scholar
  19. 19.
    D. Kapur and H. Zhang. RRL: A User's Manual. General Electric Corporate Research and Development, Schenectady, NY, March 1986. Unpublished Manuscript.Google Scholar
  20. 20.
    D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, pages 333–354, December 1983.Google Scholar
  21. 21.
    Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT '95: Workshop on Industrial-Strength Formal specification Techniques, Boca Raton, FL, 1995. IEEE Computer Society. To appear.Google Scholar
  22. 22.
    Paul S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Memorandum 110167, NASA Langley Research Center, 1995.Google Scholar
  23. 23.
    S. Owe, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. Three volumes: Language, System, and Prover Reference Manuals.Google Scholar
  24. 24.
    L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, Cambridge, England, 1987.Google Scholar
  25. 25.
    Lawrence C. Paulson. Isabelle: A generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.Google Scholar
  26. 26.
    G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115–116, 1981.Google Scholar
  27. 27.
    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, Lecture Notes in Computer Science, Liege, Belgium, June 1995. Springer-Verlag. To appear.Google Scholar
  28. 28.
    N. Shankar. A lazy approach to compositional verification. Technical Report SRI-CSL-93-8, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993.Google Scholar
  29. 29.
    R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith. STP: A mechanized logic for specification and verification. In D. Loveland, editor, 6th International Conference on Automated Deduction (CADE), volume 138 of Lecture Notes in Computer Science, New York, NY, 1982. Springer-Verlag.Google Scholar
  30. 30.
    Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Natarajan Shankar
    • 1
  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations