Advertisement

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems

  • Zohar Manna
  • Nikolaj S. Bjørner
  • Anca Browne
  • Michael Colón
  • Bernd Finkbeiner
  • Mark Pichora
  • Henny B. Sipma
  • Tomás E. Uribe
Conference paper
Part of the Advances in Computing Science book series (ACS)

Abstract

The Stanford Temporal Prover, STeP, is a tool for the computer-aided formal verification of reactive systems, including real-time and hybrid systems, based on their temporal specification. STeP integrates methods for deductive and algorithmic verification, including model checking, theorem proving, automatic invariant generation, abstraction and modular reasoning. We describe the most recent version of STeP, Version 2.0.

Keywords

Model Check Decision Procedure Verification Condition Symbolic Model Checker Progress Property 
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. [ABL96]
    J.R. Abrial, E. Boerger, and H. Langmaack, editors. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, vol. 1165 of LNCS. Springer-Verlag, 1996.Google Scholar
  2. [BBC+95]
    N.S. Bjørner, A. Browne, E.S. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User’s Manual. Technical Report STAN-CS-TR-95–1562, Computer Science Department, Stanford University, November 1995.Google Scholar
  3. [BBC+96]
    N.S. Bjørner, A. Browne, E.S. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In R. Alur and T.A. Henzinger, editors, Proc. 8th Intl. Conference on Computer Aided Verification, vol. 1102 of LNCS, pages 415–418. Springer-Verlag, July 1996.Google Scholar
  4. [BBM97]
    N.S. Bjorner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):4987, February 1997. Preliminary version appeared in 1st Intl. Conf. on Principles and Practice of Constraint Programming, vol. 976 of LNCS, pp. 589623, Springer-Verlag, 1995.Google Scholar
  5. [Bjø98]
    N.S. Ajmer. Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University, November 1998.Google Scholar
  6. [BLM97]
    N.S. Bjørner, U. Lerner, and Z. Manna Deductive verification of parameterized fault-tolerant systems: A case study. In Intl. Conf. on Temporal Logic. Kluwer, 1997. To appear.Google Scholar
  7. [BMS95]
    A. Browne, Z. Manna, and H.B. Sipma. Generalized temporal verification diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, vol. 1026 of LNCS, pages 484–498. Springer-Verlag, 1995.Google Scholar
  8. [BMSU98]
    N.S. Bjørner, Z. Manna, H.B. Sipma, and T.E. Uribe. Deductive verification of real-time systems using STeP. Technical report, Computer Science Department, Stanford University, October 1998. Preliminary version appeared in 4th Intl. AMAST Workshop on Real-Time Systems, vol. 1231 of LNCS, pages 22–43. Springer-Verlag, May 1997.Google Scholar
  9. [BP98]
    N.S. Bjørner and M.C. Pichora. Deciding fixed and non-fixed size bitvectors. In 4th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 1384 of LNCS, pages 376–392. Springer-Verlag, 1998.Google Scholar
  10. [BSU97]
    N.S. Bjørner, M.E. Stickel, and T.E. Uribe. A practical integration of first-order reasoning and decision procedures. In Proc. of the 14th Intl. Conference on Automated Deduction,vol. 1249 of LNCS,pages 101–115. Springer-Verlag, July 1997.Google Scholar
  11. [CFO89]
    D. Cantone, A. Ferro, and E. Omodeo. Computable Set Theory. Oxford Sceince Publications, 1989.MATHGoogle Scholar
  12. [CLS96]
    D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak’s decision procedure for combinations of theories. In Proc. of the 13th Intl. Conference on Automated Deduction, vol. 1104 of LNCS,pages 463–477. Springer-Verlag, 1996.Google Scholar
  13. [CU98]
    M.A. Colón and T.E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In A.J. Hu and M.Y. Vardi, editors, Proc. 10th Intl. Conference on Computer Aided Verification, vol. 1427 of LNCS, pages 293–304. Springer-Verlag, July 1998.Google Scholar
  14. [CZ98]
    D. Cantone and C.G. Zarba. A new fast tableau-based decision procedure for an unquantified fragment of set theory. In Int. Workshop on First-Order Theorem Proving (FTP’98), 1998. 188Google Scholar
  15. [FMS98]
    B. Finkbeiner, Z. Manna, and H.B. Sipma. Deductive verification of modular systems. In W.P. de Roever, H. Langmaack, and A. Pnueli, editors, Compositionality: The Significant Difference, COMPOS’97, vol. 1536 of LNCS, pages 239–275. Springer-Verlag, 1998.CrossRefGoogle Scholar
  16. [HP95]
    N. Halbwachs and Y.E. Proy. POLyhedra desK cAlculator (POLKA). VERIMAG, Montbonnot, France, September 1995.Google Scholar
  17. [MAB+94]
    Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E.S. Chang, M. Colón, L. de Alfaro, H. Devarajan, H.B. Sipma, and T.E. Uribe. STeP: The Stanford temporal prover. Technical Report STAN-CS-TR-94–1518, Computer Science Department, Stanford University, July 1994.Google Scholar
  18. [MBSU98]
    Z. Manna, A. Browne, H.B. Sipma, and T.E. Uribe. Visual abstractions for temporal verification. In AMAST’98, LNCS. Springer-Verlag, 1998. To appear.Google Scholar
  19. [MCF+98]
    Z. Manna, M.A. Colón, B. Finkbeiner, H.B. Sipma, and T.E. Uribe. Abstraction and modular verification of infinite-state reactive systems. In M. Broy, editor, Requirements Targeting Software and Systems Engineering (RTSE),LNCS. Springer-Verlag, 1998. To appear.Google Scholar
  20. [McM93]
    K.L. McMillan. Symbolic Model Checking. Kluwer Academic Pub., 1993.CrossRefMATHGoogle Scholar
  21. [MP94]
    Z. Manna and A. Pnueli. Temporal verification diagrams. In M. Hagiya and J.C. Mitchell, editors, Proc. International Symposium on Theoretical Aspects of Computer Software,vol. 789 of LNCS, pages 726–765. Springer-Verlag, 1994.CrossRefGoogle Scholar
  22. [MP95]
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.CrossRefGoogle Scholar
  23. [MP96]
    Z. Manna and A. Pnueli. Clocked transition systems. Technical Report STAN-CS-TR-96–1566, Computer Science Department, Stanford University, April 1996.Google Scholar
  24. [MS98]
    Z. Manna and H.B. Sipma. Deductive verification of hybrid systems using STeP. In T. Henzinger and S. Sastry, editors, Hybrid Systems: Computation and Control, vol. 1386 of LNCS, pages 305–318. Springer-Verlag, 1998.CrossRefGoogle Scholar
  25. [Sho84]
    R.E. Shostak. Deciding combinations of theories. J. ACM, 31(1):1–12, January 1984.MathSciNetCrossRefMATHGoogle Scholar
  26. [SUM98]
    H.B. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. To appear in Formal Methods in System Design, 1998. Preliminary version appeared in Proc. 8th Intl. Conference on Computer Aided Verification,vol. 1102 of LNCS, Springer-Verlag, pp. 208–219, 1996.Google Scholar
  27. [Uri98]
    T.E. Uribe. Abstraction-based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Computer Science Department, Stanford University, December 1998.Google Scholar
  28. [Wei97]
    V. Weispfenning. Quantifier elimination for real algebra—the quadratic case and beyond. In Applied Algebra and Error-Correcting Codes (AAECC) 8, pages 85–101, 1997.MathSciNetMATHGoogle Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Zohar Manna
    • 1
  • Nikolaj S. Bjørner
    • 1
  • Anca Browne
    • 1
  • Michael Colón
    • 1
  • Bernd Finkbeiner
    • 1
  • Mark Pichora
    • 1
  • Henny B. Sipma
    • 1
  • Tomás E. Uribe
    • 1
  1. 1.Computer Science DepartmentStanford UniversityStanfordUSA

Personalised recommendations