Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich (2018):
Deductive Software Verification – The KeY Book: From Theory to Practice.
Lecture Notes in Computer Science 10001.
Springer, Berlin,
doi:10.1007/978-3-319-49812-6.
Mike Barnett, K. Rustan M. Leino & Wolfram Schulte (2004):
The Spec# Programming System: An Overview.
In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), Marseille, France, March 10-14, 2004,
Lecture Notes in Computer Science 3362.
Springer, Berlin, Germany,
pp. 49–69,
doi:10.1007/978-3-540-30569-9_3.
Jasmin C. Blanchette & Tobias Nipkow (2010):
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder.
In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving (ITP 2010),
Springer LNCS 6172,
pp. 131–146,
doi:10.1007/978-3-642-14052-5_11.
François Bobot, Jean-Christophe Filliâtre, Claude Marché & Andrei Paskevich (2011):
Why3: Shepherd Your Herd of Provers.
In: Boogie 2011: First International Workshop on Intermediate Verification Languages,
Wrocław, Poland,
pp. 53–64.
http://proval.lri.fr/publications/boogie11final.pdf.
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.
Available at RISCAL.
Michael Butler (2016):
Abstract State Machines, Alloy, B, TLA, VDM, and Z, 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings.
Springer LNCS 9675,
doi:10.1007/978-3-319-33600-8.
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith & Roderick Bloem (2018):
Handbook of Model Checking.
Springer,
Berlin, Germany,
doi:10.1007/978-3-319-10575-8.
David R. Cok (2011):
OpenJML: JML for Java 7 by Extending OpenJDK.
In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: NASA Formal Methods (NFM 2011), Pasadena, CA, USA, April 18–20, 2011,
Lecture Notes in Computer Science 6617.
Springer, Berlin, Germany,
pp. 472–479,
doi:10.1007/978-3-642-20398-5_35.
Stephen H. Edwards & Manuel A. Perez-Quinones (2008):
Web-CAT: Automatically Grading Programming Assignments.
In: 13th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE '08).
ACM,
Madrid, Spain, June 30 – July 2,
pp. 328,
doi:10.1145/1384271.1384371.
See also http://web-cat.org.
Daniel Jackson (2011):
Software Abstractions — Logic, Language, and Analysis,
revised edition.
MIT Press,
Cambridge, MA, USA.
Available at http://softwareabstractions.org/.
Leslie Lamport (2002):
Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.
Addison-Wesley Longman,
Amsterdam, The Netherlands.
Available at http://research.microsoft.com/users/lamport/tla/book.html.
K. Rustan M. Leino (2010):
Dafny: An Automatic Program Verifier for Functional Correctness.
In: Edmund M. Clarke & Andrei Voronkov: Logic Programming and Automated Reasoning (LPAR-16), Dakar, Senegal, April 25–May 1, 2010,
Lecture Notes in Computer Science 6355.
Springer, Berlin, Germany,
pp. 348–370,
doi:10.1007/978-3-642-17511-4_20.
Lucas Payr (2018):
Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models.
Bachelor thesis.
Research Institute for Symbolic Computation (RISC),
Johannes Kepler University, Linz, Austria.
Available at RISCAL.
Colin Runciman, Matthew Naylor & Fredrik Lindblad (2008):
Smallcheck and Lazy Smallcheck: Automatic Exhaustive Testing for Small Values.
In: First ACM SIGPLAN Symposium on Haskell,
Haskell '08.
ACM,
New York, NY, USA,
pp. 37–48,
doi:10.1145/1411286.1411292.
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.
In: Pedro Quaresma & Ralph-Johan Back: Proceedings ThEdu'11, CTP Components for Educational Software, Wroc\IeCł aw, Poland, July 31, 2011,
EPTCS 79,
pp. 124–142,
doi:10.4204/EPTCS.79.8.
Wolfgang Schreiner (2017):
The RISC Algorithm Language (RISCAL) — Tutorial and Reference Manual (Version 1.0).
Technical Report.
RISC,
Johannes Kepler University, Linz, Austria.
Available at RISCAL.
Wolfgang Schreiner (2018):
Validating Mathematical Theories and Algorithms with RISCAL.
In: F. Rabe, W. Farmer, G. Passmore & A. Youssef: CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13–17,
Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence 11006.
Springer, Berlin,
pp. 248–254,
doi:10.1007/978-3-319-96812-4_21.
Wolfgang Schreiner (2018):
WebEx: Web Exercises for RISCAL.
Technical Report.
RISC,
Johannes Kepler University, Linz, Austria.
Available at RISCAL.
Wolfgang Schreiner, Alexander Brunhuemer & Christoph Fürst (2018):
Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models.
In: Pedro Quaresma & Walther Neuper: Post-Proceedings ThEdu'17, Theorem proving components for Educational software, Gothenburg, Sweden, August 6, 2017,
EPTCS 267,
pp. 120–139,
doi:10.4204/EPTCS.267.8.
Wolfgang Schreiner & William Steingartner (2018):
Visualizing Execution Traces in RISCAL.
Technical Report.
RISC,
Johannes Kepler University, Linz, Austria.
Available at RISCAL.
Wolfgang Schreiner & William Steingartner (2018):
Visualizing Logic Formula Evaluation in RISCAL.
Technical Report.
RISC,
Johannes Kepler University, Linz, Austria.
Available at RISCAL.
Dominique Thiébaut (2015):
Automatic Evaluation of Computer Programs Using Moodle's Virtual Programming Lab (VPL) Plug-in.
Journal of Computing Sciences in Colleges 30(6),
pp. 145–151.
Available at http://dl.acm.org/citation.cfm?id=2753024.2753053.
Susilo Veri Yulianto & Inggriani Liem (2014):
Automatic Grader for Programming Assignment using Source Code Analyzer.
In: International Conference on Data and Software Engineering (ICODSE).
IEEE,
Bandung, Indonesia, November 26–27,
pp. 1–4,
doi:10.1109/ICODSE.2014.7062687.