PVS: Combining specification, proof checking, and model checking | SpringerLink
Skip to main content
Springer Nature Link
Log in

PVS: Combining specification, proof checking, and model checking

  • Conference paper
  • First Online:
Formal Methods in Computer-Aided Design (FMCAD 1996)

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

Included in the following conference series:

Abstract

We claim that no single technique such as rewriting, BDDs, or model checking is effective for all aspects of hardware verification. Many examples need the careful integration of these techniques. We have shown some simple examples to illustrate the integration available in PVS. This combination of techniques has been applied to some larger examples such as an SRT divider and Rockwell-Collins AAMP series of processors. The automation available in PVS on these examples can be further improved through the use of more decision procedures (e.g., bit vectors) and better verification methodologies (e.g., abstraction, induction).

The development of PVS was funded by SRI International through IR&D funds. Various applications and customizations have been funded by NSF Grant CCR-930044, NASA, ARPA contract A721, and NRL contract N00015-92-C-2177. The PVS system is the result of developed as a collaborative effort involving Sam Owre, John Rushby, Mandayam Srivas, David Cyrluk, Pat Lincoln, Sree Rajan, Judy Crow, among many others.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

  2. R. L. Constable, S. P. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendier, 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 

  3. D. Cyrluk. Inverting the abstraction mapping: A methodology for hardware verification. In Proceedings of Formal Methods in Computer Aided Design (FMCAD '96), 1996. This volume.

    Google Scholar 

  4. D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design (TPCD '94), volume 910 of Lecture Notes in Computer Science, pages 203–222, Bad Herrenalb, Germany, September 1994. Springer-Verlag.

    Google Scholar 

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

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

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

    Google Scholar 

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

    Google Scholar 

  9. 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, pages 2–16, Boca Raton, FL, 1995. IEEE Computer Society.

    Google Scholar 

  10. Paul S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Memorandum 110167, NASA Langley Research Center, 1995.

    Google Scholar 

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

    Google Scholar 

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

  13. H. Rueß, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, number 1102 in Lecture Notes in Computer Science, pages 123–134, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  14. Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    N. Shankar

Authors
  1. N. Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mandayam Srivas Albert Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Shankar, N. (1996). PVS: Combining specification, proof checking, and model checking. In: Srivas, M., Camilleri, A. (eds) Formal Methods in Computer-Aided Design. FMCAD 1996. Lecture Notes in Computer Science, vol 1166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031813

Download citation

  • DOI: https://doi.org/10.1007/BFb0031813

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61937-6

  • Online ISBN: 978-3-540-49567-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation