1. Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta & Laurent Voisin (2010): Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer 12(6), pp. 447–466, doi:10.1007/s10009-010-0145-y.
  2. Yves Bertot & Pierre Castéran (2016): Interactive Theorem Proving and Program Development — CoqArt: The Calculus of Inductive Constructions. Springer, Berlin, Germany, doi:10.1007/978-3-662-07964-5.
  3. Alexander Brunhuemer (2017): Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models. Bachelor thesis. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria.
  4. Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky & Wolfgang Windsteiger (2016): Theorema 2.0: Computer-Assisted Natural-Style Mathematics. Journal of Formalized Reasoning 9(1), pp. 149–185, doi:10.6092/issn.1972-5787/4568.
  5. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino & Erik Poll (2005): An Overview of JML Tools and Applications. International Journal on Software Tools for Technology Transfer 7(3), pp. 212–232, doi:10.1007/s10009-004-0167-4.
  6. Jon Barwise Dave Barker-Plummer, John Etchemendy & Albert Liu (2008): Tarski's World: Revised and Expanded. CSLI Publications, Stanford, CA, USA.
  7. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 — Where Programs Meet Provers. In: M. Felleisen & P. Gardner: ESOP 2013, Rome, Italy, March 16-24, 2013, Lecture Notes in Computer Science 7792. Springer, Berlin, Germany, pp. 125–128, doi:10.1007/978-3-642-37036-6_8.
  8. Christoph Fürst & Wolfgang Schreiner (2017): Formalization of Two Algorithms Arising in Number Theory. Technical Report. RISC, Johannes Kepler University, Linz, Austria. To appear.
  9. Daniel Jackson (2011): Software Abstractions — Logic, Language, and Analysis, revised edition. MIT Press, Cambridge, MA, USA.
  10. Leslie Lamport (2002): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston, MA, USA.
  11. Peter G. Larsen & John Fitzgerald (2016): The Evolution of VDM Tools from the 1990s to 2015 and the Influence of CAMILA. J. Logical and Algebr. Meth. in Prog. 85(5), pp. 985–998, doi:10.1016/j.jlamp.2015.10.001.
  12. K. Rustan M. Leino (2010): Dafny: An Automatic Program Verifier for Functional Correctness. In: E. M. Clarke & A. Voronkov: LPAR-16, Dakar, Senegal, April 25–May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science 6355. Springer, pp. 348–370, doi:10.1007/978-3-642-17511-4_20.
  13. Tobias Nipkow & Gerwin Klein (2014): Concrete Semantics — With Isabelle/HOL. Springer, Heidelberg, Germany, doi:10.1007/978-3-319-10542-0.
  14. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2017): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, Berlin, Germany. Available at
  15. RISCAL (2017): The RISC Algorithm Language (RISCAL). Available at
  16. Daniela Ritirc (2016): Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools. RISC, Johannes Kepler University, Linz, Austria.
  17. Wolfgang Schreiner (2009): The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom. Formal Aspects of Computing 21(3), pp. 277–291, doi:10.1007/s00165-008-0069-4.
  18. Wolfgang Schreiner (2012): Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs. EPTCS 79, pp. 124–142, doi:10.4204/EPTCS.79.8. ThEdu'11, Wroc\IeCł aw, Poland, July 31, 2011.
  19. Wolfgang Schreiner (2017): The RISC Algorithm Language (RISCAL) — Tutorial and Reference Manual (Version 1.0). Technical Report. RISC, Johannes Kepler University, Linz, Austria. Download from RISCAL.

Comments and questions to:
For website issues: