Document Open Access Logo

An Expressive Trace Logic for Recursive Programs

Authors Dilian Gurov , Reiner Hähnle

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.21.pdf
  • Filesize: 0.89 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Operational semantics
  • Theory of computation → Program specifications
  • Theory of computation → Program verification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
Keywords
  • Denotational semantics
  • compositional semantics
  • program specification
  • compositional verification
  • fixed point logic
  • trace logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed points, for precise specification of programs with recursive procedures. Both programs and trace formulas are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.

Cite As Get BibTex

Dilian Gurov and Reiner Hähnle. An Expressive Trace Logic for Recursive Programs. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.21

Author Details

Dilian Gurov
  • KTH Royal Institute of Technology, Stockholm, Sweden
Reiner Hähnle
  • Technical University of Darmstadt, Germany

References

  1. Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, and Leonid Libkin. First-order and temporal logics for nested words. Log. Methods Comput. Sci., 4(11):1-44, 2008. URL: https://doi.org/10.2168/LMCS-4(4:11)2008.
  2. Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, and Matteo Maffei. Verifying relational properties using trace logic. In Clark W. Barrett and Jin Yang, editors, Formal Methods in Computer Aided Design, FMCAD, pages 170-178, San Jose, CA, USA, 2019. IEEE. URL: https://doi.org/10.23919/FMCAD.2019.8894277.
  3. Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification. Technical Report Version 1.17, CEA and INRIA, 2021. URL: https://frama-c.com/download/frama-c-acsl-implementation.pdf.
  4. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.
  5. Richard Bubel, Dilian Gurov, Reiner Hähnle, and Marco Scaletta. Trace-based deductive verification. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023), volume 94 of EPiC Series in Computing, pages 73-95. EasyChair, 2023. URL: https://doi.org/10.29007/VDFD.
  6. Xiaohong Chen, Dorel Lucanu, and Grigore Rosu. Matching logic explained. Journal of Logical and Algebraic Methods in Programming, 120:100638, 2021. URL: https://doi.org/10.1016/J.JLAMP.2021.100638.
  7. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. Google Scholar
  8. Patrick Cousot and Radhia Cousot. Temporal abstract interpretation. In Mark N. Wegman and Thomas W. Reps, editors, Proc. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, pages 12-25. ACM, 2000. URL: https://doi.org/10.1145/325694.325699.
  9. Mads Dam and Dilian Gurov. μ-calculus with explicit points and approximations. J. of Logic and Computation, 12(2):255-269, April 2002. URL: https://doi.org/10.1093/LOGCOM/12.2.255.
  10. Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen, Violet Ka I Pun, and Silvia Lizeth Tapia Tarifa. Locally abstract, globally concrete semantics of concurrent programming languages. In Cláudia Nalon and Renate Schmidt, editors, Proc. 26th Intl. Conf. on Automated Reasoning with Tableaux and Related Methods, volume 10501 of LNCS, pages 22-43, Cham, September 2017. Springer. URL: https://doi.org/10.1007/978-3-319-66902-1_2.
  11. Gidon Ernst, Alexander Knapp, and Toby Murray. A Hoare logic with regular behavioral specifications. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation, 11th Intl. Symp., ISoLA, Rhodes, Greece, Proc. Part I, volume 13701 of LNCS, pages 45-64. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-19849-6_4.
  12. Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. Temporal stream logic: Synthesis beyond the bools. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification: 31st Intl. Conf., CAV, Part I, volume 11561 of LNCS, pages 609-629, New York City, NY, USA, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-25540-4_35.
  13. Lars-Åke Fredlund, Dilian Gurov, Thomas Noll, Mads Dam, Thomas Arts, and Gennady Chugunov. A verification tool for Erlang. Journal of Software Tools for Technology Transfer, 4(4):405-420, August 2003. URL: https://doi.org/10.1007/S100090100071.
  14. Dilian Gurov and Reiner Hähnle. An expressive trace logic for recursive programs. CoRR, abs/2411.13125, 2024. URL: https://doi.org/10.48550/arXiv.2411.13125.
  15. Reiner Hähnle and Marieke Huisman. Deductive verification: from pen-and-paper proofs to industrial tools. In Bernhard Steffen and Gerhard Woeginger, editors, Computing and Software Science: State of the Art and Perspectives, volume 10000 of LNCS, pages 345-373. Springer, Cham, Switzerland, 2019. Google Scholar
  16. Joseph Y. Halpern and Yoav Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38(4):935-962, 1991. URL: https://doi.org/10.1145/115234.115351.
  17. Niklas Heidler and Reiner Hähnle. A Sequent Calculus for Trace Formula Implication. arXiv CoRR, May 2025. URL: https://doi.org/10.48550/arXiv.2505.03693.
  18. C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In Erwin Engeler, editor, Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pages 102-116. Springer, Berlin, Heidelberg, 1971. URL: https://doi.org/10.1007/BFb0059696.
  19. Dexter Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3):427-443, 1997. URL: https://doi.org/10.1145/256167.256195.
  20. Dexter Kozen. On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic, 1(1):60-76, 2000. URL: https://doi.org/10.1145/343369.343378.
  21. Martin Lange and Rafał Somla. Propositional dynamic logic of context-free programs and fixpoint logic with chop. Information Processing Letters, 100(2):72-75, 2006. URL: https://doi.org/10.1016/J.IPL.2006.04.019.
  22. Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, Daniel M. Zimmerman, and Werner Dietl. JML Reference Manual, May 2013. Draft revision 2344. URL: http://www.eecs.ucf.edu/~leavens/JML//OldReleases/jmlrefman.pdf.
  23. Angelika Mader. Verification of modal properties using Boolean equation systems. PhD thesis, Technical University Munich, 1997. Google Scholar
  24. Markus Müller-Olm. A modal fixpoint logic with chop. In Theoretical Aspects of Computer Science (STACS 1999), volume 1563 of LNCS, pages 510-520, Berlin Heidelberg, 1999. Springer. URL: https://doi.org/10.1007/3-540-49116-3_48.
  25. Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational semantics for While. In Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of LNCS, pages 375-390, Berlin Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-03359-9_26.
  26. Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, London, 2007. URL: https://doi.org/10.1007/978-1-84628-692-6.
  27. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, Berlin Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  28. David Michael Ritchie Park. Finiteness is mu-ineffable. Theoretical Computer Science, 3(2):173-181, 1976. URL: https://doi.org/10.1016/0304-3975(76)90022-0.
  29. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17-139, 2004. Google Scholar
  30. Damien Pous. Kleene algebra with tests and Coq tools for while programs. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, 4th Intl. Conf. ITP, Rennes, France, volume 7998 of LNCS, pages 180-196. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  31. Grigore Rosu. Matching logic. Logical Methods in Computer Science, 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:28)2017.
  32. Colin Stirling. Modal and temporal logics. In Handbook of Logic in Computer Science (Vol. 2): Background: Computational Structures, pages 477-563, USA, 1993. Oxford University Press, Inc. Google Scholar
  33. Alfred Tarski. A lattice-theoretical fixedpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  34. David von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13):1173-1214, 2001. URL: https://doi.org/10.1002/CPE.598.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact