Andrei Arusoaie (2014):
A Generic Framework for Symbolic Execution: Theory and Applications..
Faculty of Computer Science, Iaşi.
Available at https://tel.archives-ouvertes.fr/tel-01094765.
Alexandru Ioan Cuza, University of Iaşi, Romania.
Andrei Arusoaie & Dorel Lucanu (2019):
Unification in Matching Logic.
In: Maurice H. ter Beek, Annabelle McIver & José N. Oliveira: Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings,
Lecture Notes in Computer Science 11800.
Springer,
pp. 502–518,
doi:10.1007/978-3-030-30942-8_30.
Andrei Arusoaie, David Nowak, Vlad Rusu & Dorel Lucanu (2017):
A Certified Procedure for RL Verification.
In: SYNASC 2017,
IEEE CPS,
Timișoara, Romania,
pp. 129–136.
Available at https://hal.inria.fr/hal-01627517.
Denis Bogdanas & Grigore Roşu (2015):
K-Java: A Complete Semantics of Java.
In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
ACM,
New York, NY, USA,
pp. 445–456.
Available at http://doi.acm.org/10.1145/2676726.2676982.
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh & Grigore Roşu (2021):
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation.
In: Proceedings of the 33rd International Conference on Computer-Aided Verification.
ACM,
pp. 477–499,
doi:10.1007/978-3-030-81688-9_23.
Xiaohong Chen, Dorel Lucanu & Grigore Roşu (2020):
Initial Algebra Semantics in Matching Logic.
Technical Report http://hdl.handle.net/2142/107781.
University of Illinois at Urbana-Champaign.
Submitted.
Xiaohong Chen, Dorel Lucanu & Grigore Roşu (2021):
Matching logic explained.
Journal of Logical and Algebraic Methods in Programming 120,
pp. 100638,
doi:10.1016/j.jlamp.2021.100638.
Xiaohong Chen & Grigore Roşu (2019):
Matching μ-logic.
In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'19).
IEEE,
Vancouver, Canada,
pp. 1–13,
doi:10.1109/LICS.2019.8785675.
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer & C. L. Talcott. (2007):
All About Maude, A High-Performance Logical Framework.
Lecture Notes in Computer Science 4350.
Springer,
doi:10.1007/978-3-540-71999-1_10.
Andrei Ştefănescu, Daejun Park, Shijiao Yuwen, Yilong Li & Grigore Roşu (2016):
Semantics-Based Program Verifiers for All Languages.
In: OOPSLA'16.
ACM,
pp. 74–91,
doi:10.1145/2983990.2984027.
Chucky Ellison & Grigore Rosu (2012):
An Executable Formal Semantics of C with Applications.
In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
New York, USA,
pp. 533–544.
Available at http://doi.acm.org/10.1145/2103656.2103719.
Chris Hathhorn, Chucky Ellison & Grigore Roşu (2015):
Defining the Undefinedness of C.
In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation,
New York, NY, USA,
pp. 336–345.
Available at http://doi.acm.org/10.1145/2737924.2737979.
Dorel Lucanu, Vlad Rusu & Andrei Arusoaie (2016):
A Generic Framework for Symbolic Execution: A Coinductive Approach.
Journal of Symbolic Computation,
pp. –,
doi:10.1016/j.jsc.2016.07.012.
Dorel Lucanu, Vlad Rusu, Andrei Arusoaie & David Nowak (2015):
Verifying Reachability-Logic Properties on Rewriting-Logic Specifications.
In: Narciso Martí-Oliet, Peter Csaba Ölveczky & Carolyn L. Talcott: Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday,
Lecture Notes in Computer Science 9200.
Springer,
pp. 451–474,
doi:10.1007/978-3-319-23165-5_21.
Alberto Martelli & Ugo Montanari (1982):
An Efficient Unification Algorithm.
ACM Transactions on Programming Languages and Systems 4(2),
pp. 258–282,
doi:10.1145/357162.357169.
Daejun Park, Andrei Ştefănescu & Grigore Roşu (2015):
KJS: A Complete Formal Semantics of JavaScript.
In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation,
New York, NY, USA,
pp. 346–356.
Available at http://doi.acm.org/10.1145/2737924.2737991.
G. Plotkin (1972):
Building in equational theories.
Machine Intelligence 7,
pp. 73–90.
Available at http://www.cs.york.ac.uk/mlg/MI/mi.html.
Http://www.cs.york.ac.uk/mlg/MI/mi.htmlJournal Webpage.
Gordon D. Plotkin (1970):
A Note on Inductive Generalization.
Machine Intelligence 5,
pp. 153–163.
Grigore Rosu (2017):
Matching Logic.
Log. Methods Comput. Sci. 13(4),
pp. 1–61,
doi:10.23638/LMCS-13(4:28)2017.
Grigore Roșu, Andrei Ștefănescu, Ştefan Ciobâcă & Brandon M. Moore (2013):
One-Path Reachability Logic.
In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013,
pp. 358–367,
doi:10.1109/LICS.2013.42.
Vlad Rusu & Andrei Arusoaie (2016):
Proving Reachability-Logic Formulas Incrementally.
In: Dorel Lucanu: Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016, April 2-3, 2016, Revised Selected Papers,
Lecture Notes in Computer Science 9942.
Springer,
pp. 134–151,
doi:10.1007/978-3-319-44802-2_8.
Andrei Stefanescu, Ştefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta & Grigore Rosu (2014):
All-Path Reachability Logic.
In: Gilles Dowek: RTA-TLCA 2014, 2014, Vienna, Austria, July 14-17, 2014. Proceedings,
LNCS 8560.
Springer,
pp. 425–440,
doi:10.1007/978-3-319-08918-8_29.
eptcs@eptcs.org