Advertisement

Towards Light-Weight Verification and Heavy-Weight Testing

  • Stephan Pfab
  • Harald Rueß
  • Sam Owre
  • Friedrich W. von Henke
Conference paper
Part of the Advances in Computing Science book series (ACS)

Abstract

Traditional, simulation-based validation methods have not kept up with the scale or pace of modern digital design, and, therefore, form a major impediment in the drive for evermore complex designs (Hardin et al.,1998). This is mainly due to the sheer number of possible test cases which makes it nearly impossible to perform exhaustive testing. Thus testing only demonstrates the existence but not the absence of flaws. Even worse, it is unlikely that testing alone would have caught errors like the famous bug in the lookup table of the Intel Pentium floating-point division unit, since it only occurred on table inputs that were thought to be beyond the region of interest (Pratt, 1995).

Keywords

Theorem Prove Formal Verification Symbolic Evaluation Abstract State Machine Common Lisp 
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. U. Berger and H. Schwichtenberg (1991): An inverse of the evaluation functional for typed A-calculus. In Proceedings, Sixth Annual IEEE Symposium On Logic in Computer Science, pages 203–211, Amsterdam, The Netherlands. IEEE Computer Society Press.CrossRefGoogle Scholar
  2. E. Börger and S. Mazzanti (1996): A Correctness Proof for Pipelining in RISC Architectures. Technical Report DIMACS 96–22, Dipartimento di Informatica, University of Pisa, Corso Italia 40, 56125 Pisa, Italy.Google Scholar
  3. R.S. Boyer and J S. Moore (1996): Mechanized Formal Reasoning about Programs and Computing Machines. In Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT Press.Google Scholar
  4. G. Dowek, A. Felty, H. Herbelin, G. Huet, Ch. Murthy, C. Parent, Chr. PaulinMohring, and B. Werner (1993): The Coq Proof Assistant User’s Guide (Version 5.8). INRIA-Rocquencourt - CNRS - ENS Lyon. Projet Formel.Google Scholar
  5. Y. Gurevich (1995): Evolving algebras 1993: Lipari guide. In E. Börger, editor, Current Trends in Theoretical Computer Science, pages 9–36. Computer Science Press.Google Scholar
  6. D. Hardin, M. Wilding, and D. Greve (1998): Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. In CAV’98: Computer-Aided Verification, Lecture Notes in Computer Science. Springer Verlag.Google Scholar
  7. S.L. Peyton, Jones and Ph. Wader (1993): Imperative Functional Programming In ACM Symposium on Principles of Programming Languages (POPL’93),pages 71–84, Charleston.CrossRefGoogle Scholar
  8. M. Kaufmann and J S. Moore (1997): An Industrial Strength Theorem Prover for a Logic based on Common Lisp. IEEE Transactions on Software Engineering, 21(4):203–213.CrossRefGoogle Scholar
  9. J S. Moore (1998): Symbolic Simulation: an ACL2 Approach. In Formal Methods in Computer-Aided Design (FMCAD ‘88), Lecture Notes in Computer Science. Springer Verlag. Accepted for publication.Google Scholar
  10. S. Owre, J. Rushby, N. Shankar, and F. von Henke (1995): Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering,21(2):107–125.CrossRefGoogle Scholar
  11. S. Owre, N. Shankar, J.M. Rushby, and D.W.J Stringer-Calvert (1998): The PVS Specification Language, Version 2.2. Computer Science Lab, SRI International, Menlo Park CA 94025. From: http://www.csl.sri.com/pvs.html.Google Scholar
  12. H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß (1996): Mechanized Semantics of Simple Imperative Programming Constructs. Ulmer Informatik-Berichte 96–11, Universität Ulm, Fakultät für Informatik.Google Scholar
  13. V. Pratt (1995) Anatomy of the Pentium Bug. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, TAPSOFT’95: Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, pages 97–107. Springer Verlag.CrossRefGoogle Scholar
  14. N. Shankar (1998): Personal communication.Google Scholar
  15. M.K. Srivas and S.P. Miller (1995): Formal Verification of the AAMP5 Microprocessor. In M.G. Hinchey and J.P. Bowen, editors, Applications of Formal Methods, International Series in Computer Science, chapter 7, pages 125–180. Prentice Hall, Hemel Hempstead, UK.Google Scholar
  16. M. Srivas, H. Rueß, and D. Cyrluk (1997) Hardware Verification using PVS. In Th. Kropf, editor, Formal Hardware Verification Methods and Systems in Comparison, volume 1287 of Lecture Notes in Computer Science, chapter 4, pages 156–205. Springer Verlag.Google Scholar
  17. M. Stegmüller (1998): Formale Verifikation des DLX RISC-Prozessors: Eine Fallstudie basierend auf abstrakten Zustandsmaschinen. Master’s thesis, Universität Ulm. From http://www.informatik.uni-ulm.de/ki/Edu/Diplomarbeiten.Google Scholar
  18. F.W. von Henke, M. Luther, H. Pfeifer, H. Rueß, D. Schwier, M. Strecker, and M. Wagner (1996): The TYPELAB specification and verification environment. In M. Nivat M. Wirsing, editor, Proceedings AMAST’96, pages 604–607. Springer LNCS 1101.Google Scholar
  19. Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß (1998): Case Studies in Meta-Level Theorem Proving. In Jim Grundy and Malcolm Newey, editors, Proc. Intl. Conf. on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science. Springer-Verlag.Google Scholar
  20. M. Wilding (1997): Robust Computer System Proofs in PVS. Presented at LFM’97: the Fourth NASA Langley Formal Methods Workshop; also available from http://www.csl.sri.com/sri-csl-fm.html.MATHGoogle Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Stephan Pfab
  • Harald Rueß
  • Sam Owre
  • Friedrich W. von Henke

There are no affiliations available

Personalised recommendations