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.
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.
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.
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.
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.
Jon Barwise Dave Barker-Plummer, John Etchemendy & Albert Liu (2008):
Tarski's World: Revised and Expanded.
CSLI Publications,
Stanford, CA, USA.
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.
Christoph Fürst & Wolfgang Schreiner (2017):
Formalization of Two Algorithms Arising in Number Theory.
Technical Report.
RISC,
Johannes Kepler University, Linz, Austria.
To appear.
Daniel Jackson (2011):
Software Abstractions — Logic, Language, and Analysis,
revised edition.
MIT Press,
Cambridge, MA, USA.
Leslie Lamport (2002):
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.
Addison-Wesley,
Boston, MA, USA.
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.
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.
Tobias Nipkow & Gerwin Klein (2014):
Concrete Semantics — With Isabelle/HOL.
Springer,
Heidelberg, Germany,
doi:10.1007/978-3-319-10542-0.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2017):
Isabelle/HOL — A Proof Assistant for Higher-Order Logic.
Springer,
Berlin, Germany.
Available at http://isabelle.in.tum.de/doc/tutorial.pdf.
Daniela Ritirc (2016):
Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools.
RISC,
Johannes Kepler University, Linz, Austria.
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.
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.
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.
eptcs@eptcs.org