Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 1996: Foundations of Software Technology and Theoretical Computer Science pp 43–51Cite as

Mechanized formal methods: Progress and prospects

  • Invited Papers
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1180))

Abstract

In the decade of the 1990s, formal methods have progressed from an academic curiosity at best, and a target of ridicule at worst, to a point where the leading manufacturer of microprocessors has indicated that its next design will be formally verified. In this short paper, I sketch a plausible history of the developments that led to this transformation, present a snapshot of the current state of the practice, and indicate some promising directions for the future. Mindful of the title of this conference, I suggest how formal methods might have an impact on software similar to that which they have had on hardware.

This work was supported by the Air Force Office of Scientific Research, Air Force Materiel Command, USAF, under contract F49620-95-C0044 and by the National Science Foundation under contract CCR-9509931.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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.

    Google Scholar 

  2. ásgeir Th. Eiríksson and Ken L. McMillan. Using formal verification/analysis methods on the critical path in system design: A case study. In Pierre Wolper, editor, Computer-Aided Verification, CAV '95, volume 939 of Lecture Notes in Computer Science, pages 367–380, Liege, Belgium, June 1995. Springer-Verlag.

    Google Scholar 

  3. Randal E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.

    Google Scholar 

  4. Randal E. Bryant. Bit-level analysis of an SRT divider circuit. In Proceedings of the 33rd Design Automation Conference, pages 661–665, Las Vegas, NV, June 1996.

    Google Scholar 

  5. E. M. Clarke, S. M. German, and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. In Alur and Henzinger [1], pages 111–122.

    Google Scholar 

  6. E. M. Clarke, Manpreet Khaira, and Xudong Zhao. Word level symbolic model checking—avoiding the Pentium FDIV error. In Proceedings of the 33rd Design Automation Conference, pages 645–648, Las Veqas, NV, June 1996.

    Google Scholar 

  7. Edmund M. Clarke, Orna Grumberg, Hiromi Haraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, and Linda A. Ness. Verification of the Futurebus+ cache coherence protocol. Formal Methods in System Design, 6(2):217–232, March 1995.

    Google Scholar 

  8. Dan Craigen, Susan Gerhart, and Ted Ralston. Formal methods reality check: Industrial usage. IEEE Transactions on Software Engineering, 21(2):90–98, February 1995.

    Google Scholar 

  9. David A. Cyrluk and Mandayam K. Srivas. Theorem proving: Not an esoteric diversion, but the unifying framework for industrial verification. In International Conference on Computer Design: VLSI in Computers and Processors (ICCD '95), pages 538–544, Austin, TX, October 1995. IEEE Computer Society.

    Google Scholar 

  10. David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In International Conference on Computer Design: VLSI in Computers and Processors, pages 522–525. IEEE Computer Society, October 1992. Cambridge, MA.

    Google Scholar 

  11. Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, volume 1051 of Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.

    Google Scholar 

  12. Mats P. E. Heimdahl. Experiences and lessons from the analysis of TCAS II. In Steven J. Zeil, editor, International Symposium on Software Testing and Analysis (ISSTA), pages 79–83, San Diego, CA, January 1996. Association for Computing Machinery.

    Google Scholar 

  13. Mats P. E. Heimdahl and Barbara J. Czerny. Using PVS to analyze hierarchical state-based requirements for completeness and consistency. In IEEE High-Assurance Systems Engineering Workshop (HASE '96), Niagara on the Lake, Canada, October 1996. To appear.

    Google Scholar 

  14. Mats P. E. Heimdahl and Nancy G. Leveson. Completeness and consistency in hierarchical state-based requirements. IEEE Transactions on Software Engineering, 22(6):363–377, June 1996.

    Google Scholar 

  15. Daniel Jackson and Craig A. Damon. Elements of style: Analyzing a software design feature with a counterexample detector. IEEE Transactions on Software Engineering, 22(7):484–495, July 1996.

    Google Scholar 

  16. Cliff B. Jones. Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, second edition, 1990.

    Google Scholar 

  17. Robyn R. Lutz. Analyzing software requirements errors in safety-critical embedded systems. In IEEE International Symposium on Requirements Engineering, pages 126–133, San Diego, CA, January 1993.

    Google Scholar 

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

    Google Scholar 

  19. Paul S. Miner and James F. Leathrum, Jr. Verification of IEEE compliant subtractive division algorithms. In Srivas [34].

    Google Scholar 

  20. J S. Moore. ACL2 theorems about commercial microprocessors. In Srivas [34].

    Google Scholar 

  21. S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Alur and Henzinger [1], pages 411–414.

    Google Scholar 

  22. Sam Owre, John Rushby, Natarajan Shankar, and Friedrich 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 

  23. Seungjoon Park and David L. Dill. An executable specification, analyzer and verifier for RMO (Relaxed Memory Order). In 7th ACM Symposium on Parallel Algorithms and Architectures, pages 34–51, July 1995.

    Google Scholar 

  24. Seungjoon Park and David L. Dill. Verification of the FLASH cache coherence protocol by aggregation of distributed transactions. In 8th ACM Symposium on Parallel Algorithms and Architectures, pages 288–296, Padua, Italy, June 1996.

    Google Scholar 

  25. Vaughan Pratt. Anatomy of the Pentium bug. In TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 97–107, Aarhus, Denmark, May 1995. Springer-Verlag.

    Google Scholar 

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

  27. H. Rue\, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In Alur and Henzinger [1], pages 123–134.

    Google Scholar 

  28. John Rushby. Automated deduction and formal methods. In Alur and Henzinger [1], pages 169–183.

    Google Scholar 

  29. John Rushby. Calculating with requirements. In 3rd IEEE International Symposium on Requirements Engineering, Annapolis, MD, January 1997. IEEE Computer Society. To appear.

    Google Scholar 

  30. N. Shankar. Computer-aided computing. In Bernhard Möller, editor, Mathematics of Program Construction '95, volume 947 of Lecture Notes in Computer Science, pages 50–66. Springer-Verlag, 1995.

    Google Scholar 

  31. Natarajan Shankar. Unifying verification paradigms. In Bengt Jonsson and Joachim Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of Lecture Notes in Computer Science, pages 22–39, Uppsala, Sweden, September 1996. Springer-Verlag.

    Google Scholar 

  32. J. M. Spivey, editor. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, second edition, 1993.

    Google Scholar 

  33. Tirumale Sreemani and Joanne M. Atlee. Feasibility of model checking software requirements. In COMPASS '96 (Proceedings of the Eleventh Annual Conference on Computer Assurance), pages 77–88, Gaithersburg, MD, June 1996. IEEE Washington Section.

    Google Scholar 

  34. M. Srivas, editor. Formal Methods in Computer-Aided Design (FMCAD '96), Palo Alto, CA, November 1996. To appear.

    Google Scholar 

  35. Mandayam K. Srivas and Steven P. Miller. Formal verification of the AAMP5 microprocessor. In Michael G. Hinchey and Jonathan P. Bowen, editors, Applications of Formal Methods, Prentice Hall International Series in Computer Science, chapter 7, pages 125–180. Prentice Hall, Hemel Hempstead, UK, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    John Rushby

Authors
  1. John Rushby
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

V. Chandru V. Vinay

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rushby, J. (1996). Mechanized formal methods: Progress and prospects. In: Chandru, V., Vinay, V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1996. Lecture Notes in Computer Science, vol 1180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62034-6_36

Download citation

  • DOI: https://doi.org/10.1007/3-540-62034-6_36

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62034-1

  • Online ISBN: 978-3-540-49631-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation