@phdthesis(arusoaie-2014,
 author       = {Andrei Arusoaie},
 year         = {2014},
 title        = {A Generic Framework for Symbolic Execution: Theory and Applications.},
 school       = {Faculty of Computer Science, Ia{\c s}i},
 url          = {https://tel.archives-ouvertes.fr/tel-01094765},
 note         = {Alexandru Ioan Cuza, University of Ia{\c{s}}i, Romania},
)
@inproceedings(fm,
 author       = {Andrei Arusoaie and Dorel Lucanu},
 year         = {2019},
 title        = {Unification in Matching Logic},
 editor       = {Maurice H. ter Beek and Annabelle McIver and Jos{\'{e}} N. Oliveira},
 booktitle    = {Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019, Porto, Portugal, October 7-11, 2019, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11800},
 publisher    = {Springer},
 pages        = {502--518},
 doi          = {10.1007/978-3-030-30942-8\_30},
)
@misc(maude-tool-for-certif-aintiunif,
 author       = {Andrei Arusoaie and Dorel Lucanu},
 year         = {2021},
 title        = {Certifying (anti)unification in Matching Logic},
 url          = {https://github.com/andreiarusoaie/certifying-unification-in-aml},
)
@inproceedings(arusoaie:hal-01627517,
 author       = {Andrei Arusoaie and David Nowak and Vlad Rusu and Dorel Lucanu},
 year         = {2017},
 title        = {{A Certified Procedure for RL Verification}},
 booktitle    = {{SYNASC 2017}},
 series       = {IEEE CPS},
 address      = {Timișoara, Romania},
 pages        = {129--136},
 url          = {https://hal.inria.fr/hal-01627517},
)
@inproceedings(DBLP:conf/popl/BogdanasR15,
 author       = {Denis Bogdanas and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {K-Java: A Complete Semantics of Java},
 booktitle    = {Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {445--456},
 url          = {http://doi.acm.org/10.1145/2676726.2676982},
)
@inproceedings(chen-lin-trinh-rosu-2021-cav,
 author       = {Xiaohong Chen and Zhengyao Lin and Minh-Thai Trinh and Ro\c{s}u, Grigore},
 year         = {2021},
 title        = {Towards a Trustworthy Semantics-Based Language Framework via Proof Generation},
 booktitle    = {Proceedings of the 33rd International Conference on Computer-Aided Verification},
 publisher    = {ACM},
 pages        = {477–499},
 doi          = {10.1007/978-3-030-81688-9_23},
)
@techreport(chen-lucanu-rosu-2020-tr,
 author       = {Xiaohong Chen and Dorel Lucanu and Ro\c{s}u, Grigore},
 year         = {2020},
 title        = {Initial Algebra Semantics in Matching Logic},
 type         = {Technical Report},
 number       = {http://hdl.handle.net/2142/107781},
 institution  = {University of Illinois at Urbana-Champaign},
 note         = {Submitted},
)
@article(chen-lucanu-rosu-2021-jlamp,
 author       = {Xiaohong Chen and Dorel Lucanu and Grigore Roşu},
 year         = {2021},
 title        = {Matching logic explained},
 journal      = {Journal of Logical and Algebraic Methods in Programming},
 volume       = {120},
 pages        = {100638},
 doi          = {10.1016/j.jlamp.2021.100638},
)
@inproceedings(CR19,
 author       = {Xiaohong Chen and Ro\c{s}u, Grigore},
 year         = {2019},
 title        = {Matching $\mu$-logic},
 booktitle    = {Proceedings of the 34\textsuperscript{th} Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'19)},
 publisher    = {IEEE},
 address      = {Vancouver, Canada},
 pages        = {1--13},
 doi          = {10.1109/LICS.2019.8785675},
)
@book(allAboutMaude,
 author       = {M.\ Clavel and F.\ Dur\'{a}n and S.\ Eker and P.\ Lincoln and Mart\'{\i}-Oliet, N.\ and J.\ Meseguer and C. L. Talcott.},
 year         = {2007},
 title        = {{All About Maude, A High-Performance Logical Framework}},
 series       = {Lecture Notes in Computer Science},
 volume       = {4350},
 publisher    = {Springer},
 doi          = {10.1007/978-3-540-71999-1_10},
)
@inproceedings(stefanescu-park-yuwen-li-rosu-2016-oopsla,
 author       = {\c{S}tef\u{a}nescu, Andrei and Daejun Park and Shijiao Yuwen and Yilong Li and Ro\c{s}u, Grigore},
 year         = {2016},
 title        = {Semantics-Based Program Verifiers for All Languages},
 booktitle    = {OOPSLA'16},
 publisher    = {ACM},
 pages        = {74--91},
 doi          = {10.1145/2983990.2984027},
)
@inproceedings(ellison-rosu-2012-popl,
 author       = {Chucky Ellison and Grigore Rosu},
 year         = {2012},
 title        = {An Executable Formal Semantics of C with Applications},
 booktitle    = {Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 address      = {New York, USA},
 pages        = {533--544},
 url          = {http://doi.acm.org/10.1145/2103656.2103719},
)
@inproceedings(DBLP:conf/pldi/HathhornER15,
 author       = {Chris Hathhorn and Chucky Ellison and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {Defining the Undefinedness of C},
 booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 address      = {New York, NY, USA},
 pages        = {336--345},
 url          = {http://doi.acm.org/10.1145/2737924.2737979},
)
@article(JSC2016,
 author       = {Dorel Lucanu and Vlad Rusu and Andrei Arusoaie},
 year         = {2016},
 title        = {{A} {G}eneric {F}ramework for {S}ymbolic {E}xecution: {A} {C}oinductive {A}pproach},
 journal      = {Journal of Symbolic Computation},
 pages        = {--},
 doi          = {10.1016/j.jsc.2016.07.012},
)
@inproceedings(DBLP:conf/birthday/LucanuRAN15,
 author       = {Dorel Lucanu and Vlad Rusu and Andrei Arusoaie and David Nowak},
 year         = {2015},
 title        = {Verifying Reachability-Logic Properties on Rewriting-Logic Specifications},
 editor       = {Mart{\'{\i}}{-}Oliet, Narciso and Peter Csaba {\"{O}}lveczky and Carolyn L. Talcott},
 booktitle    = {Logic, Rewriting, and Concurrency - Essays dedicated to Jos{\'{e}} Meseguer on the Occasion of His 65th Birthday},
 series       = {Lecture Notes in Computer Science},
 volume       = {9200},
 publisher    = {Springer},
 pages        = {451--474},
 doi          = {10.1007/978-3-319-23165-5\_21},
)
@article(martelli,
 author       = {Alberto Martelli and Ugo Montanari},
 year         = {1982},
 title        = {An Efficient Unification Algorithm},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {4},
 number       = {2},
 pages        = {258--282},
 doi          = {10.1145/357162.357169},
)
@inproceedings(park-stefanescu-rosu-2015-pldi,
 author       = {Daejun Park and {\c S}tef\u{a}nescu, Andrei and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {KJS: A Complete Formal Semantics of JavaScript},
 booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 address      = {New York, NY, USA},
 pages        = {346--356},
 url          = {http://doi.acm.org/10.1145/2737924.2737991},
)
@article(Plo:72,
 author       = {G. Plotkin},
 year         = {1972},
 title        = {Building in equational theories},
 journal      = {Machine Intelligence},
 volume       = {7},
 pages        = {73--90},
 url          = {http://www.cs.york.ac.uk/mlg/MI/mi.html},
 note         = {Http://www.cs.york.ac.uk/mlg/MI/mi.htmlJournal Webpage},
)
@article(Plotkin70,
 author       = {Gordon D. Plotkin},
 year         = {1970},
 title        = {A Note on Inductive Generalization},
 journal      = {Machine Intelligence},
 volume       = {5},
 pages        = {153--163},
)
@article(rosu-2017-lmcs,
 author       = {Grigore Rosu},
 year         = {2017},
 title        = {Matching Logic},
 journal      = {Log. Methods Comput. Sci.},
 volume       = {13},
 number       = {4},
 pages        = {1--61},
 doi          = {10.23638/LMCS-13(4:28)2017},
)
@inproceedings(DBLP:conf/lics/RosuSCM13,
 author       = {Grigore Roșu and Andrei Ștefănescu and \c{S}tefan Ciob\^ac\u{a} and Brandon M. Moore},
 year         = {2013},
 title        = {One-Path Reachability Logic},
 booktitle    = {28th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS} 2013, New Orleans, LA, USA, June 25-28, 2013},
 pages        = {358--367},
 doi          = {10.1109/LICS.2013.42},
)
@inproceedings(DBLP:conf/wrla/RusuA16,
 author       = {Vlad Rusu and Andrei Arusoaie},
 year         = {2016},
 title        = {Proving Reachability-Logic Formulas Incrementally},
 editor       = {Dorel Lucanu},
 booktitle    = {Rewriting Logic and Its Applications - 11th International Workshop, {WRLA} 2016, April 2-3, 2016, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {9942},
 publisher    = {Springer},
 pages        = {134--151},
 doi          = {10.1007/978-3-319-44802-2\_8},
)
@inproceedings(stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta,
 author       = {Andrei Stefanescu and Ciob{\^{a}}c{\u{a}}, {\c{S}}tefan and Radu Mereuta and Brandon M. Moore and Traian{-}Florin Serbanuta and Grigore Rosu},
 year         = {2014},
 title        = {All-Path Reachability Logic},
 editor       = {Gilles Dowek},
 booktitle    = {{RTA-TLCA} 2014, 2014, Vienna, Austria, July 14-17, 2014. Proceedings},
 series       = {LNCS},
 volume       = {8560},
 publisher    = {Springer},
 pages        = {425--440},
 doi          = {10.1007/978-3-319-08918-8\_29},
)
@misc(checkermm,
 author       = {K Team},
 title        = {Matching Logic Proof Checker},
 url          = {https://github.com/kframework/matching-logic-proof-checker/blob/main/theory/matching-logic-250-loc.mm},
)