Skip to main content
SpringerLink
Log in

Dynamic Logic with Trace Semantics

  • Conference paper
Automated Deduction – CADE-24 (CADE 2013)

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

Included in the following conference series:

Abstract

Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic (DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae.

Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications.

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. Abadi, M., Manna, Z.: Nonclausal deduction in first-order temporal logic. Journal of the ACM 37(2), 279–317 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  3. Beckert, B.: A dynamic logic for Java Card. In: Proceedings, 2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France, pp. 111–119 (2000)

    Google Scholar 

  4. Beckert, B., Bruns, D.: Dynamic trace logic: Definition and proofs. Tech. Rep. 2012-10, Karlsruhe Institute of Technology, Department of Computer Science (2012), revised version available at http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf

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

    Google Scholar 

  6. 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 

  7. Goré, R.: Tableau methods for modal and temporal logics. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297–396. Kluwer Academic Publishers, Dordrecht (1999)

    Chapter  Google Scholar 

  8. Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, pp. 497–604. D. Reidel Publishing Co., Dordrecht (1984)

    Chapter  Google Scholar 

  9. Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Computer 18(2) (February 1985)

    Google Scholar 

  10. 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 

  11. Reynolds, M., Dixon, C.: Theorem-proving for discrete temporal logic. In: Fisher, D.M., Gabbay, Vila, L. (eds.) Handbook of Temporal Reasoning in Artificial Intelligence. Elsevier Science (2005)

    Google Scholar 

  12. Scheben, C., Schmitt, P.H.: Verification of information flow properties of java programs without approximations. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 232–249. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Combi, C., Leucker, M., Wolter, F. (eds.) Eighteenth International Symposium on Temporal Representation and Reasoning, TIME 2011, pp. 99–106. IEEE (2011)

    Google Scholar 

  14. Thums, A., Schellhorn, G., Ortmeier, F., Reif, W.: Interactive verification of statecharts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 355–373. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Wolper, P.: The tableau method for temporal logic: An overview. Logique et Analyse 28(110-111), 119–136 (1985)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Karlsruhe Institute of Technology (KIT), Germany

    Bernhard Beckert & Daniel Bruns

Authors
  1. Bernhard Beckert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniel Bruns
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15, 37134, Verona, Italy

    Maria Paola Bonacina

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beckert, B., Bruns, D. (2013). Dynamic Logic with Trace Semantics. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38574-2_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38573-5

  • Online ISBN: 978-3-642-38574-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation