A Dynamic Logic with Traces and Coinduction | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Dynamic Logic with Traces and Coinduction

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9323))

Abstract

Dynamic Logic with Traces and Coinduction is a new program logic that has an explicit syntactic representation of both programs and their traces. This allows to prove properties involving programs as well as traces. Moreover, we use a coinductive semantics which makes it possible to reason about non-terminating programs and infinite traces, such as controllers and servers. We develop a sound sequent calculus for our logic that realizes symbolic execution of the programs under verification. The calculus has been developed with the goal of automation in mind. One of the novelties of the calculus is a coinductive invariant rule for while loops that is able to prove termination as well as non-termination.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

  1. Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” revisited: On branching versus linear time temporal logic. Journal of the ACM 33, 151–178 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  2. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing. MIT Press, October 2000

    Google Scholar 

  3. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  4. Beckert, B., Mostowski, W.: A Program Logic for Handling JAVA CARD’s Transaction Mechanism. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 246–260. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Hähnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 151–171. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Combi, C., Leucker, M., Wolter, F. (eds.) 18th Intl. Symp. on Temporal Representation and Reasoning, pp. 99–106. IEEE (2011)

    Google Scholar 

  7. Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 626–641. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 457–471. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 315–329. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488–506. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Logical Methods in Computer Science 11(1), 1–32 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  12. Chang Din, C., Bubel, R., Hähnle, R.: KeY-ABS: A deductive verification tool for the concurrent modelling language ABS. In: Felty, A., Middeldorp, A. (eds.) CADE-25. LNCS (LNAI), pp. 517–526. Springer, Heidelberg (2015)

    Google Scholar 

  13. Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011)

    Google Scholar 

  14. Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422–436. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Jeffrey, A., Rathke, J.: Java JR: Fully abstract trace semantics for a core java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423–438. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Velroyen, H., Rümmer, P.: Non-termination checking for imperative programs. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 154–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technische Universität Darmstadt, Darmstadt, Germany

    Richard Bubel, Crystal Chang Din & Reiner Hähnle

  2. FireEye, Dresden, Germany

    Keiko Nakata

Authors
  1. Richard Bubel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Crystal Chang Din
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Reiner Hähnle
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Keiko Nakata
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Richard Bubel .

Editor information

Editors and Affiliations

  1. Uniwersytet Wrocławski, Wrocław, Poland

    Hans De Nivelle

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Bubel, R., Din, C.C., Hähnle, R., Nakata, K. (2015). A Dynamic Logic with Traces and Coinduction. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24312-2_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24311-5

  • Online ISBN: 978-3-319-24312-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation