@article(ALARCON2007105,
 author       = {Beatriz Alarcon and Raul Gutierrez and Jose Iborra and Salvador Lucas},
 year         = {2007},
 title        = {Proving Termination of Context-Sensitive Rewriting with {MU-TERM}},
 journal      = {ENTCS},
 volume       = {188},
 pages        = {105 -- 115},
 doi          = {10.1016/j.entcs.2007.05.041},
)
@inproceedings(ceta,
 author       = {Martin Avanzini and Christian Sternagel and Ren{\'e} Thiemann},
 year         = {2015},
 title        = {{Certification of Complexity Proofs using CeTA}},
 booktitle    = {RTA},
 series       = {LIPIcs},
 volume       = {36},
 pages        = {23--39},
 doi          = {10.4230/LIPIcs.RTA.2015.23},
 url          = {http://drops.dagstuhl.de/opus/volltexte/2015/5187},
)
@inproceedings(variance-popl2007,
 author       = {Josh Berdine and Aziem Chawdhary and Byron Cook and Dino Distefano and Peter O'Hearn},
 year         = {2007},
 title        = {Variance Analyses from Invariance Analyses},
 booktitle    = {POPL},
 pages        = {211--224},
 doi          = {10.1145/1190216.1190249},
)
@inproceedings(DBLP:conf/popl/BogdanasR15,
 author       = {Bogd\u{a}na\c{s}, Denis and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {{K}-{J}ava: A Complete Semantics of {J}ava},
 booktitle    = {{POPL}},
 pages        = {445--456},
 doi          = {10.1145/2676726.2676982},
)
@inproceedings(termination-cav2013,
 author       = {Marc Brockschmidt and Byron Cook and Carsten Fuhs},
 year         = {2013},
 title        = {Better Termination Proving through Cooperation},
 booktitle    = {CAV},
 pages        = {413--429},
 doi          = {10.1007/978-3-642-39799-8\_28},
)
@inproceedings(t2-tacas2016,
 author       = {Marc Brockschmidt and Byron Cook and Samin Ishtiaq and Heidy Khlaaf and Nir Piterman},
 year         = {2016},
 title        = {{T2}: Temporal Property Verification},
 booktitle    = {TACAS},
 pages        = {387--393},
 doi          = {10.1007/978-3-662-49674-9\_22},
)
@article(Cao2018,
 author       = {Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Andrew W. Appel},
 year         = {2018},
 title        = {{VST-Floyd}: A Separation Logic Tool to Verify Correctness of {C} Programs},
 journal      = {JAR},
 doi          = {10.1007/s10817-018-9457-5},
)
@inproceedings(ijcar-2018,
 author       = {\c{S}tefan Ciob\^ac\u{a} and Dorel Lucanu},
 year         = {2018},
 title        = {A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems},
 booktitle    = {{IJCAR}},
 pages        = {295--311},
 doi          = {10.1007/978-3-319-94205-6\_20},
)
@inproceedings(DBLP:conf/synasc/Ciobaca14,
 author       = {Ciob\^ac\u{a}, {\c{S}}tefan},
 year         = {2014},
 title        = {Reducing Partial Equivalence to Partial Correctness},
 booktitle    = {{SYNASC}},
 pages        = {164--171},
 doi          = {10.1109/SYNASC.2014.30},
)
@techreport(rmt,
 author       = {Ciob\^ac\u{a}, {\c S}tefan and Dorel Lucanu},
 year         = {2016},
 title        = {{RMT}: Proving Reachability Properties in Constrained Term Rewriting Systems Modulo Theories},
 type         = {Technical Report},
 number       = {TR 16-01},
 institution  = {Alexandru Ioan Cuza University, Faculty of Computer Science},
)
@inproceedings(contejean07frocos,
 author       = {Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
 year         = {2007},
 title        = {Certification of Automated Termination Proofs},
 booktitle    = {{FroCoS}},
 pages        = {148--162},
 doi          = {10.1007/978-3-540-74621-8\_10},
)
@inproceedings(terminator-pldi2006,
 author       = {Byron Cook and Andreas Podelski and Andrey Rybalchenko},
 year         = {2006},
 title        = {Termination Proofs for Systems Code},
 booktitle    = {PLDI},
 pages        = {415--426},
 doi          = {10.1145/1133981.1134029},
)
@inproceedings(ramsey-tacas2013,
 author       = {Byron Cook and Abigail See and Florian Zuleger},
 year         = {2013},
 title        = {Ramsey vs. Lexicographic Termination Proving},
 booktitle    = {TACAS},
 pages        = {47--61},
 doi          = {10.1007/978-3-642-36742-7\_4},
)
@inproceedings(stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta,
 author       = {\c{S}tef\u{a}nescu, Andrei and Ciob\^{a}c\u{a}, {\c{S}}tefan and Mereu\c{t}\u{a}, Radu and Brandon M. Moore and \c{S}erb\u{a}nu\c{t}\u{a}, Traian Florin and Ro\c{s}u, Grigore},
 year         = {2014},
 title        = {All-Path Reachability Logic},
 booktitle    = {RTA-TLCA},
 pages        = {425--440},
 doi          = {10.1007/978-3-319-08918-8\_29},
)
@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},
 pages        = {74--91},
 doi          = {10.1145/2983990.2984027},
)
@inproceedings(ellison-rosu-2012-popl,
 author       = {Chucky Ellison and Ro{\c s}u, Grigore},
 year         = {2012},
 title        = {An Executable Formal Semantics of {C} with Applications},
 booktitle    = {{POPL}},
 pages        = {533--544},
 doi          = {10.1145/2103656.2103719},
)
@article(Giesl2017,
 author       = {J{\"u}rgen Giesl and Cornelius Aschermann and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Jera Hensel and Carsten Otto and Martin Pl{\"u}cker and Schneider-Kamp, Peter and Thomas Str{\"o}der and Stephanie Swiderski and Ren{\'e} Thiemann},
 year         = {2017},
 title        = {Analyzing Program Termination and Complexity Automatically with {AProVE}},
 journal      = {JAR},
 volume       = {58},
 number       = {1},
 pages        = {3--31},
 doi          = {10.1007/s10817-016-9388-y},
)
@article(JSC2016,
 author       = {Dorel Lucanu and Vlad Rusu and Andrei Arusoaie},
 year         = {2017},
 title        = {A generic framework for symbolic execution: a coinductive approach},
 journal      = {J. Symb. Comput.},
 volume       = {80},
 pages        = {125--163},
 doi          = {10.1016/j.jsc.2016.07.012},
)
@inproceedings(da2016modular,
 author       = {Pedro da Rocha Pinto and Dinsdale-Young, Thomas and Philippa Gardner and Julian Sutherland},
 year         = {2016},
 title        = {Modular Termination Verification for Non-Blocking Concurrency},
 booktitle    = {ESOP},
 pages        = {176--201},
 doi          = {10.1007/978-3-662-49498-1\_8},
)
@inproceedings(rosu-stefanescu-2012-oopsla,
 author       = {Ro\c{s}u, Grigore and \c{S}tef\u{a}nescu, Andrei},
 year         = {2012},
 title        = {Checking Reachability using Matching Logic},
 booktitle    = {OOPSLA},
 pages        = {555--574},
 doi          = {10.1145/2384616.2384656},
)
@inproceedings(rosu-stefanescu-ciobaca-moore-2013-lics,
 author       = {Ro\c{s}u, Grigore and \c{S}tef\u{a}nescu, Andrei and Ciob\^{a}c\u{a}, {\c S}tefan and Brandon M. Moore},
 year         = {2013},
 title        = {One-Path Reachability Logic},
 booktitle    = {LICS},
 pages        = {358--367},
 doi          = {10.1109/LICS.2013.42},
)
@inproceedings(rosu-ellison-schulte-2010-amast,
 author       = {Ro\c{s}u, Grigore and Chucky Ellison and Wolfram Schulte},
 year         = {2010},
 title        = {Matching Logic: An Alternative to {H}oare/{F}loyd Logic},
 booktitle    = {AMAST},
 series       = {LNCS},
 volume       = {6486},
 pages        = {142--162},
 doi          = {10.1007/978-3-642-17796-5\_9},
)
@article(schmidt2010closures,
 author       = {Schmidt-Schau{\ss}, Manfred and David Sabel},
 year         = {2010},
 title        = {Closures of may-, should-and must-convergences for contextual equivalence},
 journal      = {Information Processing Letters},
 volume       = {110},
 number       = {6},
 pages        = {232--235},
 doi          = {10.1016/j.ipl.2010.01.001},
)
@article(DBLP:journals/iandc/SerbanutaRM09,
 author       = {{\c S}erb{\u a}nu{\c t}{\u a}, Traian Florin and Ro{\c s}u, Grigore and Jos{\'e} Meseguer},
 year         = {2009},
 title        = {A Rewriting Logic Approach to Operational Semantics},
 journal      = {{I}nformation and {C}omputation},
 volume       = {207},
 number       = {2},
 pages        = {305--340},
 doi          = {10.1016/j.ic.2008.03.026},
)
@inproceedings(key-ifm2017,
 author       = {Dominic Steinh{\"o}fel and Nathan Wasser},
 year         = {2017},
 title        = {A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows},
 booktitle    = {iFM},
 pages        = {279--294},
 doi          = {10.1007/978-3-319-66845-1\_18},
)
@misc(winskel1993formal,
 author       = {Glynn Winskel},
 year         = {1993},
 title        = {The formal semantics of programming languages. Foundations of Computing},
)