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