@book(DBLP:series/txtcs/BertotC04,
 author       = {Yves Bertot and Pierre Cast{\'{e}}ran},
 year         = {2004},
 title        = {Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions},
 series       = {Texts in Theoretical Computer Science. An {EATCS} Series},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-07964-5},
)
@inproceedings(DBLP:conf/esop/BlanchetteBL0T17,
 author       = {Jasmin Christian Blanchette and Aymeric Bouzy and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel},
 year         = {2017},
 title        = {Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants},
 booktitle    = {{ESOP}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10201},
 publisher    = {Springer},
 pages        = {111--140},
 doi          = {10.1016/0304-3975(91)90043-2},
)
@inproceedings(DBLP:conf/cade/CiobacaL18,
 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}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {295--311},
 doi          = {10.1016/j.ic.2008.03.026},
)
@inproceedings(DBLP:conf/types/Gimenez94,
 author       = {Eduardo Gim{\'{e}}nez},
 year         = {1994},
 title        = {Codifying Guarded Definitions with Recursive Schemes},
 booktitle    = {{TYPES}},
 series       = {Lecture Notes in Computer Science},
 volume       = {996},
 publisher    = {Springer},
 pages        = {39--59},
 doi          = {10.1007/3-540-60579-7_3},
)
@article(DBLP:journals/cacm/Hoare69,
 author       = {C. A. R. Hoare},
 year         = {1969},
 title        = {An Axiomatic Basis for Computer Programming},
 journal      = {Commun. {ACM}},
 volume       = {12},
 number       = {10},
 pages        = {576--580},
 doi          = {10.1145/363235.363259},
)
@inproceedings(DBLP:conf/popl/HurNDV13,
 author       = {Chung{-}Kil Hur and Georg Neis and Derek Dreyer and Viktor Vafeiadis},
 year         = {2013},
 title        = {The power of parameterization in coinductive proof},
 booktitle    = {{POPL}},
 publisher    = {{ACM}},
 pages        = {193--206},
)
@article(DBLP:journals/jsc/LucanuRA17,
 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(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},
 booktitle    = {Logic, Rewriting, and Concurrency},
 series       = {Lecture Notes in Computer Science},
 volume       = {9200},
 publisher    = {Springer},
 pages        = {451--474},
 doi          = {10.1007/978-3-319-02654-1_16},
)
@inproceedings(DBLP:conf/esop/MoorePR18,
 author       = {Brandon M. Moore and Pe{\~{n}}a, Lucas and Grigore Rosu},
 year         = {2018},
 title        = {Program Verification by Coinduction},
 booktitle    = {{ESOP}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10801},
 publisher    = {Springer},
 pages        = {589--618},
 doi          = {10.1145/2480359.2429093},
)
@book(DBLP:books/sp/NipkowPW02,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
 series       = {Lecture Notes in Computer Science},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9_6},
)
@article(DBLP:journals/cacm/OHearn19,
 author       = {Peter W. O'Hearn},
 year         = {2019},
 title        = {Separation logic},
 journal      = {Commun. {ACM}},
 volume       = {62},
 number       = {2},
 pages        = {86--95},
 doi          = {10.1145/3211968},
)
@book(DBLP:books/cu/RoeverBH2001,
 author       = {Willem P. de Roever and Frank S. de Boer and Ulrich Hannemann and Jozef Hooman and Yassine Lakhnech and Mannes Poel and Job Zwiers},
 year         = {2001},
 title        = {Concurrency Verification: Introduction to Compositional and Noncompositional Methods},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 volume       = {54},
 publisher    = {Cambridge University Press},
)
@inproceedings(DBLP:conf/lics/RosuSCM13,
 author       = {Grigore Rosu and Andrei Stefanescu and \c{S}tefan Ciob\^ac\u{a} and Brandon M. Moore},
 year         = {2013},
 title        = {One-Path Reachability Logic},
 booktitle    = {{LICS}},
 publisher    = {{IEEE} Computer Society},
 pages        = {358--367},
)
@inproceedings(DBLP:conf/tase/RusuGH18,
 author       = {Vlad Rusu and Gilles Grimaud and Micha{\"{e}}l Hauspie},
 year         = {2018},
 title        = {Proving Partial-Correctness and Invariance Properties of Transition-System Models},
 booktitle    = {{TASE}},
 publisher    = {{IEEE} Computer Society},
 pages        = {60--67},
)
@unpublished(rusu:hal-01962912,
 author       = {Vlad Rusu and Gilles Grimaud and Micha{\"e}l Hauspie},
 year         = {2019},
 title        = {{Proving Partial-Correctness and Invariance Properties of Transition-System Models}},
 url          = {https://hal.inria.fr/hal-01962912},
)
@book(sangiorgi2011,
 author       = {Davide Sangiorgi},
 year         = {2011},
 title        = {Introduction to Bisimulation and Coinduction},
 publisher    = {Cambridge University Press},
 address      = {New York, NY, USA},
 doi          = {10.1017/CBO9780511777110},
)
@inproceedings(DBLP:conf/lopstr/SkeirikSM17,
 author       = {Stephen Skeirik and Andrei Stefanescu and Jos{\'{e}} Meseguer},
 year         = {2017},
 title        = {A Constructor-Based Reachability Logic for Rewrite Theories},
 booktitle    = {{LOPSTR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10855},
 publisher    = {Springer},
 pages        = {201--217},
 doi          = {10.1007/978-3-319-08918-8_29},
)
@article(DBLP:journals/lmcs/StefanescuCMMSR19,
 author       = {Andrei Stefanescu and \c{S}tefan Ciob\^ac\u{a} and Radu Mereuta and Brandon M. Moore and Traian{-}Florin Serbanuta and Grigore Rosu},
 year         = {2019},
 title        = {All-Path Reachability Logic},
 journal      = {Logical Methods in Computer Science},
 volume       = {15},
 number       = {2},
)
@inproceedings(DBLP:conf/oopsla/StefanescuPYLR16,
 author       = {Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu},
 year         = {2016},
 title        = {Semantics-based program verifiers for all languages},
 booktitle    = {{OOPSLA}},
 publisher    = {{ACM}},
 pages        = {74--91},
 doi          = {10.1145/2983990.2984027},
)