Skip to main content
SpringerLink
Log in

Proving the Refuted: Symbolic Model Checkers as Proof Generators

  • Chapter
Concurrency, Compositionality, and Correctness

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5930))

Abstract

The paper presents an automatic method to derive a deductive proof of response properties from symbolic model checking. The method is based on a new proof rule for response properties that deals directly with compassion (strong fairness). The method can be applied to infinite-state systems. In particular, model checking of response of (predicate- and ranking-) abstracted heap programs is automatically transformed into a deductive proof for the concrete heap system. All examples presented in the paper were run in tlv.

This research was supported in part by ONR grant N00014-99-1-0131, and SRC grant 2004-TJ-1256.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Balaban, I.: Shape Analysis by Augmentation, Abstraction, and Transformation. PhD thesis, New York University, New York (May 1987)

    Google Scholar 

  2. Balaban, I., Pnueli, A., Zuck, L.D.: Modular ranking abstraction. Int. J. Found. Comput. Sci. 18(1), 5–44 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  3. Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  4. Emerson, E., Clarke, E.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  5. Fang, Y., Piterman, N., Pnueli, A., Zuck, L.D.: Liveness with invisible ranking. Software Tools for Technology Transfer 8(3), 261–279 (2006)

    Article  MATH  Google Scholar 

  6. Kesten, Y., Pnueli, A.: A Compositional Approach to CTL* Verification. Theor. Comp. Sci. 331(2-3), 397–428 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  7. Kupferman, O., Vardi, M.: From complementation to certification. Theor. Comp. Sci. 345, 83–100 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  8. Kurshan, R.: Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1995)

    Book  MATH  Google Scholar 

  9. Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. Princ. of Prog. Lang., pp. 97–107 (1985)

    Google Scholar 

  10. Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  11. Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comp. Sci. 83(1), 97–130 (1991)

    Article  MATH  Google Scholar 

  12. McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)

    Book  MATH  Google Scholar 

  13. Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Namjoshi, K.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 174–188. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Peled, D., Zuck, L.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 1–14. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Pnueli, A., Sa’ar, Y.: All you need is compassion. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 233–247. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. First IEEE Symp. Logic in Comp. Sci., pp. 332–344 (1986)

    Google Scholar 

  20. Zuck, L., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures 30(3-4), 139–169 (2004)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. WorldEvolved Services, New York, USA

    Ittai Balaban

  2. New York University, New York, USA

    Amir Pnueli

  3. Weizmann Institute of Science (Emeritus), Israel

    Amir Pnueli

  4. University of Illinois at Chicago, USA

    Lenore D. Zuck

Authors
  1. Ittai Balaban
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lenore D. Zuck
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Bell Laboratories, 600 Mountain Ave., 07974, Murray Hill, NJ, USA

    Dennis Dams

  2. Computer Science Department, University of Bremen, P.O. Box 330440, 28334, Bremen, Germany

    Ulrich Hannemann

  3. Faculty of Mathematics and Natural Sciences, Department of Computer Science, University of Oslo, P.O. Box 1080, 0316, Blindern, Oslo, Norway

    Martin Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Balaban, I., Pnueli, A., Zuck, L.D. (2010). Proving the Refuted: Symbolic Model Checkers as Proof Generators. In: Dams, D., Hannemann, U., Steffen, M. (eds) Concurrency, Compositionality, and Correctness. Lecture Notes in Computer Science, vol 5930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11512-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11512-7_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11511-0

  • Online ISBN: 978-3-642-11512-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation