{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,7]],"date-time":"2026-04-07T11:07:41Z","timestamp":1775560061645,"version":"3.50.1"},"reference-count":40,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,5,24]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Complex frameworks for defining programming languages aim to generate various tools (e.g. interpreters, symbolic execution engines, deductive verifiers, etc.) using only the formal definition of a language. When used at an industrial scale, these tools are constantly updated, and at the same time, it is required to be trustworthy. Ensuring the correctness of such a framework is practically impossible. A solution is to generate proof objects as correctness artefacts that can be checked by an external trusted checker. A logic suitable for developing such frameworks is matching logic. K framework is a canonical example having matching logic-based foundation. Since the (symbolic) configurations of the programs are represented by matching logic patterns, the algorithms computing the dynamics of these configurations can be seen as pattern transformers and a proof object should be generated for the relationship between these patterns. In this paper, we show that conjunctions and disjunctions of patterns, produced by semantics or analysis rules, can be safely normalized using unification and antiunification algorithms. We also provide a prototype implementation of our proof object generation technique and a checker for certifying the generated objects.<\/jats:p>","DOI":"10.1093\/jigpal\/jzad008","type":"journal-article","created":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T21:51:16Z","timestamp":1683150676000},"page":"534-571","source":"Crossref","is-referenced-by-count":1,"title":["Proof-carrying parameters in certified symbolic execution"],"prefix":"10.1093","volume":"32","author":[{"given":"Andrei","family":"Arusoaie","sequence":"first","affiliation":[{"name":"Department of Computer Science, Alexandru Ioan Cuza, University of Ia\u015fi , Gen. Berthelot, 16, 700483 Ia\u015fi, Romania, andrei.arusoaie@gmail.com"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Alexandru Ioan Cuza, University of Ia\u015fi , Gen. Berthelot, 16, 700483 Ia\u015fi, Romania, dorel.lucanu@gmail.com"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2023,5,1]]},"reference":[{"key":"2024052423355329300_ref1","first-page":"502","article-title":"Unification in matching logic","volume-title":"Formal Methods - the Next 30 Years - Third World Congress, FM 2019","author":"Arusoaie","year":"2019"},{"key":"2024052423355329300_ref2","volume-title":"Certifying (Anti) Unification in Matching Logic","author":"Arusoaie","year":"2021"},{"key":"2024052423355329300_ref3","first-page":"129","article-title":"A certified procedure for RL verification","volume-title":"SYNASC 2017","author":"Arusoaie","year":"2017"},{"key":"2024052423355329300_ref4","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","article-title":"Unification theory","volume-title":"Handbook of Automated Reasoning (in 2 Volumes)","author":"Baader","year":"2001"},{"key":"2024052423355329300_ref5","first-page":"57","article-title":"Nominal anti-unification","volume-title":"26th International Conference on Rewriting Techniques and Applications, RTA 2015","author":"Baumgartner","year":"2015"},{"key":"2024052423355329300_ref6","first-page":"17","article-title":"Mechanizing matching logic in coq","volume-title":"Proceedings of the Sixth Working Formal Methods Symposium, FROM 2022","author":"Bereczky","year":"2022"},{"key":"2024052423355329300_ref7","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art the Calculus of Inductive Constructions","author":"Bertot","year":"2010"},{"key":"2024052423355329300_ref8","first-page":"445","article-title":"K-java: A complete semantics of java","volume-title":"Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201815","author":"Bogdanas","year":"2015"},{"key":"2024052423355329300_ref9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-81688-9_23","article-title":"Towards a trustworthy semantics-based language framework via proof generation","volume-title":"Proceedings of the 33rd International Conference on Computer-Aided Verification","author":"Chen","year":"2021"},{"key":"2024052423355329300_ref10","article-title":"Initial algebra semantics in matching logic","volume-title":"Technical Report","author":"Chen","year":"2020"},{"key":"2024052423355329300_ref11","doi-asserted-by":"crossref","first-page":"100638","DOI":"10.1016\/j.jlamp.2021.100638","article-title":"Matching logic explained","volume":"120","author":"Chen","year":"2021","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"2024052423355329300_ref12","first-page":"1","article-title":"Matching $\\mu $-logic","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201919)","author":"Chen","year":"2019"},{"key":"2024052423355329300_ref13","first-page":"1","article-title":"Towards a unified proof framework for automated fixpoint reasoning using matching logic","volume-title":"PACMPL Issue OOPSLA 2020","author":"Chen","year":"2020"},{"key":"2024052423355329300_ref14","volume-title":"All about Maude, a High-Performance Logical Framework","author":"Clavel","year":"2007"},{"key":"2024052423355329300_ref15","first-page":"425","article-title":"Traian florin \u015eerb\u0103nu\u0163\u0103 and Grigore Ro\u015fu. All-path reachability logic","volume-title":"RTA-TLCA","author":"\u015etef\u0103nescu","year":"2014"},{"key":"2024052423355329300_ref16","first-page":"74","article-title":"Semantics-based program verifiers for all languages","volume-title":"Proceedings of the 31st Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA\u201916)","author":"\u015etef\u0103nescu","year":"2016"},{"key":"2024052423355329300_ref17","first-page":"533","article-title":"An executable formal semantics of c with applications","volume-title":"Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201812","author":"Ellison","year":"2012"},{"key":"2024052423355329300_ref18","first-page":"336","article-title":"Defining the undefinedness of c","volume-title":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201815","author":"Hathhorn","year":"2015"},{"key":"2024052423355329300_ref19","first-page":"260","article-title":"Coming to terms with quantified reasoning","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Kov\u00e1cs","year":"2017"},{"key":"2024052423355329300_ref20","article-title":"Lean backend for K","author":"Leu\u00e7tean","journal-title":"IDLS project"},{"key":"2024052423355329300_ref21","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.jsc.2016.07.012","article-title":"A generic framework for symbolic execution: A coinductive approach","volume":"80","author":"Lucanu","year":"2016","journal-title":"Journal of Symbolic Computation"},{"key":"2024052423355329300_ref22","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/978-3-319-23165-5_21","article-title":"Verifying reachability-logic properties on rewriting-logic specifications","volume-title":"Logic, Rewriting, and Concurrency\u2014Essays Dedicated to Jos\u00e9 Meseguer on the Occasion of his 65th Birthday","author":"Lucanu","year":"2015"},{"key":"2024052423355329300_ref23","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/978-3-031-17715-6_19","article-title":"A matching logic foundation for alk","volume-title":"Theoretical Aspects of Computing\u2014ICTAC 2022: 19th International Colloquium","author":"Lungu","year":"2022"},{"key":"2024052423355329300_ref24","first-page":"262","article-title":"Chapter 23 axiomatizable classes of locally free algebras of various types","volume-title":"The Metamathematics of Algebraic Systems","author":"Mal\u2019cev","year":"1971"},{"key":"2024052423355329300_ref25","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2024052423355329300_ref26","first-page":"346","article-title":"Kjs: A complete formal semantics of javascript","volume-title":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201815","author":"Park","year":"2015"},{"key":"2024052423355329300_ref27","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1109\/LICS.1989.39186","article-title":"Elf: A language for logic definition and verified metaprogramming","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201889)","author":"Pfenning","year":"1989"},{"key":"2024052423355329300_ref28","first-page":"74","article-title":"Unification and anti-unification in the calculus of constructions","volume-title":"Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS \u201891)","author":"Pfenning","year":"1991"},{"key":"2024052423355329300_ref29","first-page":"73","article-title":"Building in equational theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"2024052423355329300_ref30","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin","year":"1970","journal-title":"Machine Intelligence"},{"key":"2024052423355329300_ref31","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-319-29473-5_8","article-title":"A mechanized textbook proof of a type unification algorithm","volume-title":"Formal Methods: Foundations and Applications","author":"Ribeiro","year":"2016"},{"key":"2024052423355329300_ref32","first-page":"1","article-title":"Matching logic","volume":"13","author":"Ro\u015fu","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"2024052423355329300_ref33","first-page":"387","article-title":"From Hoare logic to matching logic reachability","volume-title":"FM 2012","author":"Ro\u015fu","year":"2012"},{"key":"2024052423355329300_ref34","first-page":"868","article-title":"Matching logic: A new program verification approach","volume-title":"Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011","author":"Ro\u00e7u","year":"2011"},{"key":"2024052423355329300_ref35","first-page":"358","article-title":"One-path reachability logic","volume-title":"28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013","author":"Ro\u00e7u","year":"2013"},{"key":"2024052423355329300_ref36","first-page":"134","article-title":"Proving reachability-logic formulas incrementally","volume-title":"Rewriting Logic and its Applications\u201411th International Workshop, WRLA 2016","author":"Rusu","year":"2016"},{"key":"2024052423355329300_ref37","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific Journal of Mathematics"},{"key":"2024052423355329300_ref38","article-title":"Haskell backend for K","author":"K Team","journal-title":"Github project"},{"key":"2024052423355329300_ref39","article-title":"Proof checkers for K","author":"K Team","journal-title":"Github project"},{"key":"2024052423355329300_ref40","article-title":"Metamath zero","author":"Metamath Zero Team"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/32\/3\/534\/57890800\/jzad008.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/32\/3\/534\/57890800\/jzad008.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,24]],"date-time":"2024-05-24T23:36:25Z","timestamp":1716593785000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/32\/3\/534\/7146273"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,1]]},"references-count":40,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2023,5,1]]},"published-print":{"date-parts":[[2024,5,24]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzad008","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2024,6]]},"published":{"date-parts":[[2023,5,1]]}}}