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