CoChat
Sign Up
Cited by 566Formal Methods in VerificationLogic, programming, and type systemsPetri Nets in System Modeling

The DOI matches its Crossref record.

Model Checking of Safety Properties

Kupferman, Orna, Vardi, Moshe Y.·2001·Formal Methods in System Design
DOI 10.1023/a:1011254632723
Open this paper in CoChat — free account

Overview

Integrity signals

Registry

Crossref · 10.1023/a:1011254632723

Cites

Statistics

Recomputing p-values needs the paper’s full text.

Verification

Claims the paper makes

We couldn’t retrieve this paper’s full text, so its claims and self-check weren’t run. The registry and citation checks still apply.

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

Citations

Cites

No references could be resolved yet.

Research works printed but not linked: 49

  1. Y. Abarbanel, I. Beer, L. Gluhovsky, S. Keidar, and Y. Wolfstal, “FoCs—Automatic generation of simulation checkers from formal specifications,” in Computer Aided Verification, Proc. 12th Int. Conference, Lecture Notes in Computer Science, Vol. 1855, Springer-Verlag, 2000, pp. 538–542. · DOI
  2. B. Alpern and F.B. Schneider, “Defining liveness,” Information Processing Letters, Vol. 21, pp. 181–185, 1985. · DOI
  3. B. Alpern and F.B. Schneider, “Recognizing safety and liveness,” Distributed Computing,Vol. 2, pp. 117–126, 1987. · DOI
  4. A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs,” in Proc. 36th Design Automaion Conference, IEEE Computer Society, 1999, pp. 317–320. · DOI
  5. 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, Vol. 98, No. 2, pp. 142–170, 1992. · DOI
  6. A. Boujjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis, “Safety for branching time,” in Proc. 18th International Colloquium on Automata Languages and Programming, LNCS, Springer-Verlag, 1991, pp. 76–92. · DOI
  7. R.S. Boyer and J.S. Moore, “Proof-checking, theorem-proving and program verification,” Technical Report 35, Institute for Computing Science and Computer Applications, University of Texas at Austin, 1983.
  8. E.M. Clarke and E.A. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic,” in Proc. Workshop on Logic of Programs, Lecture Notes in Computer Science, Vol. 131, Springer-Verlag, 1981, pp. 52–71. · DOI
  9. E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244–263, 1986. · DOI
  10. W. Canfield, E.A. Emerson, and A. Saha, “Checking formal specifications under simulation,” in Proc. International Conference on Computer Design, 1997, pp. 455–460. · DOI
  11. A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer, “Alternation,” Journal of the Association for Computing Machinery, Vol. 28, No. 1, pp. 114–133, 1981. · DOI
  12. C. Courcoubetis, M.Y. Vardi, P Wolper, and M. Yannakakis, “Memory efficient algorithms for the verification of temporal properties,” Formal Methods in System Design, Vol. 1, pp. 275–288, 1992. · DOI
  13. E.A. Emerson, “Alternative semantics for temporal logics,” Theoretical Computer Science, Vol. 26, pp. 121–130, 1983. · DOI
  14. E.A. Emerson, “Temporal and modal logic,” in Handbook of Theoretical Computer Science, 1990, pp. 997–1072. · DOI
  15. N. Francez, Program Verification. International Computer Science, Addison-Weflay, 1992.
  16. R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper, “Simple on-the-fly automatic verification of linear temporal logic,” in P. Dembiski and M. Sredniawa (Eds), Protocol Specification, Testing, and Verification, Chapman & Hall, 1995, pp. 3–18. · DOI
  17. P. Godefroid and P. Wolper, “Using partial orders for the efficient verification of deadlock freedom and safety properties,” in Proc. 3rd Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 575, Springer-Verlag, 1991, pp. 332–342. · DOI
  18. R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi, “A new heuristic for bad cycle detection using BDDs,” in Computer Aided Verification, Proc. 9th Int. Conference, Lecture Notes in Computer Science, Vol. 1254, Springer-Verlag, 1997, pp. 268–278. · DOI
  19. H. Iwashita and T. Nakata, “Forward model checking techniques oriented to buggy designs,” in Proc. IEEE/ACM International Conference on Computer Aided Design, 1997, pp. 400–404. · DOI
  20. N. Klarlund, “Mona & Fido: The logic-automaton connection in practice,” in Computer Science Logic, CSL '97, Lecture Notes in Computer Science, 1998. · DOI
  21. O. Kupferman and M.Y. Vardi, “Weak alternating automata are not that weak,” in Proc. 5th Israeli Symposium on Theory of Computing and Systems, IEEE Computer Society Press, 1997, pp. 147–158. · DOI
  22. O. Kupferman and M.Y. Vardi, “Freedom, weakness, and determinism: From linear-time to branching-time,” in Proc. 13th IEEE Symposium on Logic in Computer Science, 1998, pp. 81–92. · DOI
  23. O. Kupferman, M.Y. Vardi, and P. Wolper, “An automata-theoretic approach to branching-time model checking,” Journal of the ACM, Vol. 47, No. 2, 2000. · DOI
  24. L. Lamport, “Logical foundation,” in Distributed systems—Methods and Tools for Specification, Lecture Notes in Computer Science, Vol. 190, Springer-Verlag, 1985.
  25. O. Lichtenstein and A. Pnueli, “Checking that finite state concurrent programs satisfy their linear specification,” in Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, 1985, pp. 97–107. · DOI
  26. Y. Luo, T. Wongsonegoro, and A. Aziz, “Hybrid techniques for fast functional simulation,” in Proc. 35th Design Automation Conference, IEEE Computer Society, 1998. · DOI
  27. Z. Manna, A. Anuchitanukul, N. Bjorner, A. Browne, E. Chang, M. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T. Uribe, “STeP: The Stanford temporal prover,” Technical Report STAN-CS-TR–94–1518, Dept. of Computer Science, Stanford University, 1994. · DOI
  28. K.L. McMillan, “Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits,” in Proc. 4th Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 663, Springer-Verlag, 1992, pp. 164–174.
  29. A.R. Meyer and M.J. Fischer, “Economy of description by automata, grammars, and formal systems,” in Proc. 12th IEEE Symp. on Switching and Automata Theory, 1971, pp. 188–191. · DOI
  30. S. Miyano and T. Hayashi, “Alternating finite automata on ω-words,” Theoretical Computer Science, Vol. 32, pp. 321–330, 1984. · DOI
  31. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, Berlin, 1992. · DOI
  32. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Safety, Springer-Verlag, New York, 1995.
  33. S. Melzer and S. Roemer, “Deadlock checking using net unfoldings,” in Computer Aided Verification, Proc. 9th Int. Conference, Lecture Notes in Computer Science, Vol. 1254, Springer-Verlag, 1997, pp. 364–375. · DOI
  34. A.R. Meyer and L.J. Stockmeyer, “The equivalence problem for regular expressions with squaring requires exponential time,” in Proc. 13th IEEE Symp. on Switching and Automata Theory, 1972, pp. 125–129. · DOI
  35. S. Owicki and L. Lamport, “Proving liveness properties of concurrent programs,” ACM Transactions on Programming Languages and Systems, Vol. 4, No. 3, pp. 455–495, 1982. · DOI
  36. J.P. Queille and J. Sifakis, “Specification and verification of concurrent systems in Cesar,” in Proc. 5th International Symp. on Programming, Lecture Notes in Computer Science, Vol. 137, Springer-Verlag, 1981, pp. 337–351.
  37. K. Ravi and F. Somenzi, “High-density reachability analysis,” in Proc. Int'l Conf. on Computer-Aided Design, San Jose, 1995, pp. 154–158. · DOI
  38. S. Safra, “On the complexity of ω-automata,” in Proc. 29th IEEE Symposium on Foundations of Computer Science, White Plains, October 1988, pp. 319–327. · DOI
  39. A.P. Sistla and E.M. Clarke, “The complexity of propositional linear temporal logic,” Journal ACM, Vol. 32, pp. 733–749, 1985. · DOI
  40. A.P. Sistla, “Satefy, liveness and fairness in temporal logic,” Formal Aspects of Computing,Vol. 6, pp. 495–511, 1994. · DOI
  41. R.E. Shankar, S. Owre, and J.M. Rushby, “The PVS proof checker: A reference manual (beta release),” Technical Report, Computer Science laboratory, SRI International, Menlo Park, California, 1993.
  42. H.J. Touati, R.K. Brayton, and R. Kurshan, “Testing language containment for ?-automata using BDD's,” Information and Computation, Vol. 118, No. 1, pp. 101–109, 1995. · DOI
  43. A. Valmari, “On-the-fly verification with stubborn sets,” in Proc. 5nd Conference on Computer Aided Verifi-cation, Lecture Notes in Computer Science, Vol. 697, Springer-Verlag, 1993. · DOI
  44. M.Y.6Vardi, “An automata-theoretic approach to linear temporal logic,” in F. Moller and G. Birtwistle (Eds.), Logics for Concurrency: Structure versus Automata, Lecture Notes in Computer Science, Vol. 1043, Springer-Verlag, Berlin, 1996, pp. 238–266. · DOI
  45. M.Y. Vardi and P. Wolper, “An automata-theoretic approach to automatic program verification,” in Proc. First Symposium on Logic in Computer Science, Cambridge, 1986, pp. 332–344.
  46. M.Y. Vardi and P. Wolper, “Automata-theoretic techniques for modal logics of programs,” Journal of Computer and System Science, Vol. 32, No. 2, pp. 182–221, 1986. · DOI
  47. M.Y. Vardi and P. Wolper, “Reasoning about infinite computations,” Information and Computation, Vol. 115, No. 1, pp. 1–37, 1994. · DOI
  48. P. Wolper, “Synthesis of Communicating Processes from Temporal Logic Specifications,” Ph.D. Thesis, Stanford University, 1982.
  49. J. Yuan, J. Shen, J. Abraham, and A. Aziz, “On combining formal and informal verification,” in Computer Aided Verification, Proc. 9th Int. Conference, Lecture Notes in Computer Science, Vol. 1254, Springer-Verlag, 1997, pp. 376–387. · DOI

Cited by

Sorted by citations

Metadata

Authors
Kupferman, O., & Vardi, M. Y.
Affiliations
  • Hebrew University of Jerusalem (IL)
  • Rice University (US)
ORCID
Venue
Formal Methods in System Design
Publisher
Springer Science and Business Media LLC
Published
2001-11
Volume
19
Issue
3
Pages
291-314
ISSN
  • 0925-9856 (ISSN-L)
  • 1572-8102
DOI
10.1023/a:1011254632723
OpenAlex
W1540883472
Cited by
566
References
0
Citations by year
2026: 11 · 2025: 27 · 2024: 35 · 2023: 33 · 2022: 20 · 2021: 44 · 2020: 32 · 2019: 32 · 2018: 32 · 2017: 28 · 2016: 31 · 2015: 33 · 2014: 36 · 2013: 29 · 2012: 18
FWCI
11.67
Type
journal article
Language
en
Open access
closed
Licence
Locations
Formal Methods in System Design (publishedVersion)
Topics
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Petri Nets in System Modeling
Keywords
model checking, safety properties, linear temporal logic, automata, Tableau, state space exploration

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review