References

  1. 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.
  2. 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.
  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.
  4. 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.
  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. Available at RISCAL.
  6. 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.
  7. 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.
  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.
  9. 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.
  10. Daniel Jackson (2011): Software Abstractions — Logic, Language, and Analysis, revised edition. MIT Press, Cambridge, MA, USA. Available at http://softwareabstractions.org/.
  11. 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.
  12. 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.
  13. 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.
  14. RISCAL (2017): The RISC Algorithm Language (RISCAL). Available at https://www.risc.jku.at/research/formal/software/RISCAL.
  15. Daniela Ritirc (2016): Formally Modeling and Analyzing Mathematical Algorithms with Software Specification Languages & Tools. RISC, Johannes Kepler University, Linz, Austria. Available at https://www.risc.jku.at/publications/download/risc_5224/Master_Thesis.pdf.
  16. 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.
  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. 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.
  19. 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.
  20. 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.
  21. Wolfgang Schreiner (2018): WebEx: Web Exercises for RISCAL. Technical Report. RISC, Johannes Kepler University, Linz, Austria. Available at RISCAL.
  22. 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.
  23. Wolfgang Schreiner & William Steingartner (2018): Visualizing Execution Traces in RISCAL. Technical Report. RISC, Johannes Kepler University, Linz, Austria. Available at RISCAL.
  24. Wolfgang Schreiner & William Steingartner (2018): Visualizing Logic Formula Evaluation in RISCAL. Technical Report. RISC, Johannes Kepler University, Linz, Austria. Available at RISCAL.
  25. 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.
  26. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org