1. Yves Bertot & Pierre Castéran (2004): Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, doi:10.1007/978-3-662-07964-5.
  2. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu & Dmitriy Traytel (2017): Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. In: ESOP, Lecture Notes in Computer Science 10201. Springer, pp. 111–140, doi:10.1016/0304-3975(91)90043-2.
  3. Ştefan Ciobâcă & Dorel Lucanu (2018): A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. In: IJCAR, Lecture Notes in Computer Science 10900. Springer, pp. 295–311, doi:10.1016/j.ic.2008.03.026.
  4. Eduardo Giménez (1994): Codifying Guarded Definitions with Recursive Schemes. In: TYPES, Lecture Notes in Computer Science 996. Springer, pp. 39–59, doi:10.1007/3-540-60579-7_3.
  5. C. A. R. Hoare (1969): An Axiomatic Basis for Computer Programming. Commun. ACM 12(10), pp. 576–580, doi:10.1145/363235.363259.
  6. Chung-Kil Hur, Georg Neis, Derek Dreyer & Viktor Vafeiadis (2013): The power of parameterization in coinductive proof. In: POPL. ACM, pp. 193–206.
  7. Dorel Lucanu, Vlad Rusu & Andrei Arusoaie (2017): A generic framework for symbolic execution: A coinductive approach. J. Symb. Comput. 80, pp. 125–163, doi:10.1016/j.jsc.2016.07.012.
  8. Dorel Lucanu, Vlad Rusu, Andrei Arusoaie & David Nowak (2015): Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. In: Logic, Rewriting, and Concurrency, Lecture Notes in Computer Science 9200. Springer, pp. 451–474, doi:10.1007/978-3-319-02654-1_16.
  9. Brandon M. Moore, Lucas Peña & Grigore Rosu (2018): Program Verification by Coinduction. In: ESOP, Lecture Notes in Computer Science 10801. Springer, pp. 589–618, doi:10.1145/2480359.2429093.
  10. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, doi:10.1007/3-540-45949-9_6.
  11. Peter W. O'Hearn (2019): Separation logic. Commun. ACM 62(2), pp. 86–95, doi:10.1145/3211968.
  12. Willem P. de Roever, Frank S. de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel & Job Zwiers (2001): Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science 54. Cambridge University Press.
  13. Grigore Rosu, Andrei Stefanescu, Ştefan Ciobâcă & Brandon M. Moore (2013): One-Path Reachability Logic. In: LICS. IEEE Computer Society, pp. 358–367.
  14. Vlad Rusu, Gilles Grimaud & Michaël Hauspie (2018): Proving Partial-Correctness and Invariance Properties of Transition-System Models. In: TASE. IEEE Computer Society, pp. 60–67.
  15. Vlad Rusu, Gilles Grimaud & Michaël Hauspie (2019): Proving Partial-Correctness and Invariance Properties of Transition-System Models. Available at
  16. Davide Sangiorgi (2011): Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA, doi:10.1017/CBO9780511777110.
  17. Stephen Skeirik, Andrei Stefanescu & José Meseguer (2017): A Constructor-Based Reachability Logic for Rewrite Theories. In: LOPSTR, Lecture Notes in Computer Science 10855. Springer, pp. 201–217, doi:10.1007/978-3-319-08918-8_29.
  18. Andrei Stefanescu, Ştefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta & Grigore Rosu (2019): All-Path Reachability Logic. Logical Methods in Computer Science 15(2).
  19. Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li & Grigore Rosu (2016): Semantics-based program verifiers for all languages. In: OOPSLA. ACM, pp. 74–91, doi:10.1145/2983990.2984027.

Comments and questions to:
For website issues: