{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:21Z","timestamp":1759017921569,"version":"3.44.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Specification languages are essential in deductive program verification, but they are usually based on first-order logic,\u00a0hence less expressive than the programs they specify. Recently, trace specification logics with fixed points that are at least\u00a0as expressive as their target programs were proposed. This makes\u00a0it possible to specify not merely pre- and postconditions, but\u00a0the whole trace of even recursive programs. Previous work established a sound and complete calculus to determine whether a program satisfies a given trace formula. However,\u00a0the applicability of the calculus and its prospects for mechanized verification rely on the ability to prove consequence between\u00a0trace formulas. We present a sound sequent calculus for proving implication (i.e. trace inclusion) between trace formulas. To handle fixed\u00a0point operations with an unknown recursive bound, fixed point induction rules are used. We also employ contracts and <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-formula synchronization. While this does not yet result in a complete calculus for trace formula implication, it is possible to prove\u00a0many non-trivial properties.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_25","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:24Z","timestamp":1758969924000},"page":"473-490","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Sequent Calculus For Trace Formula Implication"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-9944-7587","authenticated-orcid":false,"given":"Niklas","family":"Heidler","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"25_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_35","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"25_CR2","doi-asserted-by":"publisher","unstructured":"Beckert, B., et al.: The Java verification tool KeY: a tutorial. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods. FM 2024. LNCS, vol. 14934, pp. 597\u2013623. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_32","DOI":"10.1007\/978-3-031-71177-0_32"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"25_CR4","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall Inc., Hoboken (1976)"},{"key":"25_CR5","doi-asserted-by":"publisher","unstructured":"Gurov, D., H\u00e4hnle, R.: An expressive trace logic for recursive programs. In: Fernandez, M. (ed.) Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction, Birmingham, UK. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2025). pre-print available at https:\/\/doi.org\/10.48550\/arXiv.2411.13125","DOI":"10.48550\/arXiv.2411.13125"},{"key":"25_CR6","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science: State of the Art and Perspectives. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"25_CR7","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Kamburjan, E., Scaletta, M.: Context-aware trace contracts. In: De\u00a0Boer, F., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Kamburjan, E. (eds.) Active Object Languages: Current Research Trends. LNCS, vol. 14360, pp. 292\u2013325. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-51060-1_11","DOI":"10.1007\/978-3-031-51060-1_11"},{"key":"25_CR8","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Scaletta, M., Kamburjan, E.: Herding CATs. In: Ferreira, C., Willemse, T.A.C. (eds.) Software Engineering and Formal Methods. SEFM 2023. LNCS, vol. 14323, pp.\u00a01\u20136. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_1","DOI":"10.1007\/978-3-031-47115-5_1"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"Automata, Languages and Programming","author":"J Halpern","year":"1983","unstructured":"Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 278\u2013291. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/BFb0036915"},{"key":"25_CR10","doi-asserted-by":"publisher","unstructured":"Heidler, N.: A Calculus for Trace Formula Implication. Master\u2019s thesis, Technical University of Darmstadt, Department of Computer Science (September 2024). https:\/\/doi.org\/10.26083\/tuprints-00029959","DOI":"10.26083\/tuprints-00029959"},{"key":"25_CR11","doi-asserted-by":"publisher","unstructured":"Heidler, N., H\u00e4hnle, R.: A Sequent Calculus for Trace Formula Implication. arXiv CoRR (May 2025). https:\/\/doi.org\/10.48550\/arXiv.2505.03693","DOI":"10.48550\/arXiv.2505.03693"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576\u2013580, 583 (1969)","DOI":"10.1145\/363235.363259"},{"key":"25_CR13","doi-asserted-by":"publisher","unstructured":"Lange, M., Stirling, C.: Model checking fixed point logic with chop. In: Nielsen, M., Engberg, U. (eds.) Foundations of Software Science and Computation Structures. FoSSaCS 2002. LNCS, vol. 2303, pp. 250\u2013263. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_18","DOI":"10.1007\/3-540-45931-6_18"},{"key":"25_CR14","doi-asserted-by":"publisher","unstructured":"McGuire, H., Manna, Z., Waldinger, R.J.: Annotation-based deduction in temporal logic. In: Gabbay, D.M., Ohlbach, H.J. (eds.) Temporal Logic, First International Conference, ICTL, Bonn, Germany. LNCS, vol.\u00a0827, pp. 430\u2013444. Springer, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFB0014003","DOI":"10.1007\/BFB0014003"},{"key":"25_CR15","doi-asserted-by":"publisher","unstructured":"M\u00fcller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 99. STACS 1999. LNCS, vol. 1563, pp. 510\u2013520. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49116-3_48","DOI":"10.1007\/3-540-49116-3_48"},{"key":"25_CR16","doi-asserted-by":"publisher","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for while. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. TPHOLs 2009. LNCS, vol.\u00a05674, pp. 375\u2013390. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_26","DOI":"10.1007\/978-3-642-03359-9_26"},{"issue":"4","key":"25_CR17","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"RJ Parikh","year":"1966","unstructured":"Parikh, R.J.: On context-free languages. J. ACM 13(4), 570\u2013581 (1966). https:\/\/doi.org\/10.1145\/321356.321364","journal-title":"J. ACM"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Sprenger, C., Dam, M.: On global induction mechanisms in a $$\\mu $$-calculus with explicit approximations. Theor. Inform. Appl. 37(4), 365\u2013391 (2003). http:\/\/www.edpsciences.org\/articles\/ita\/pdf\/2003\/04\/ita0317.pdf","DOI":"10.1051\/ita:2003024"},{"key":"25_CR19","doi-asserted-by":"publisher","unstructured":"Walukiewicz, I.: On completeness of the mu-calculus. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS), Montreal, Canada, pp. 136\u2013146. IEEE Computer Society (1993). https:\/\/doi.org\/10.1109\/LICS.1993.287593","DOI":"10.1109\/LICS.1993.287593"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:26Z","timestamp":1758969926000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}