1. Alessandro Armando, Jacopo Mantovani & Lorenzo Platania (2009): Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. 11(1), pp. 69–83, doi:10.1007/s10009-008-0091-0.
  2. Clark Barrett, Pascal Fontaine & Cesare Tinelli: SMTLib 2.6 Theory Definitions. Available at
  3. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2021): The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at
  4. Martin Brain, Cesare Tinelli, Philipp Rümmer & Thomas Wahl (2015): An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. In: 22nd IEEE Symposium on Computer Arithmetic. IEEE, pp. 160–167, doi:10.1109/ARITH.2015.26.
  5. Cristian Cadar, Daniel Dunbar & Dawson R. Engler (2008): KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In: Richard Draves & Robbert van Renesse: 8th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, pp. 209–224. Available at
  6. Edmund M. Clarke, Daniel Kroening & Flavio Lerda (2004): A Tool for Checking ANSI-C Programs. In: Kurt Jensen & Andreas Podelski: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, Lecture Notes in Computer Science 2988. Springer, pp. 168–176, doi:10.1007/978-3-540-24730-2_15.
  7. Raymond Lister (2001): Objectives and objective assessment in CS1. In: Henry MacKay Walker, Renée A. McCauley, Judith L. Gersting & Ingrid Russell: Proceedings of the 32rd SIGCSE Technical Symposium on Computer Science Education. ACM, pp. 292–296, doi:10.1145/364447.364605.
  8. Raymond Lister (2011): Concrete and Other Neo-Piagetian Forms of Reasoning in the Novice Programmer. In: Proceedings of the Thirteenth Australasian Computing Education Conference - Volume 114, ACE '11. Australian Computer Society, Inc., AUS, pp. 9–18.
  9. Leonardo de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  10. Corina S. Pasareanu, Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person & Mark Pape (2008): Combining Unit-Level Symbolic Execution and System-Level Concrete Execution for Testing Nasa Software. ISSTA'08. Association for Computing Machinery, New York, NY, USA, pp. 15–26, doi:10.1145/1390630.1390635.
  11. Barry K. Rosen, Mark N. Wegman & F. Kenneth Zadeck (1988): Global Value Numbers and Redundant Computations. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '88. Association for Computing Machinery, New York, NY, USA, pp. 12–27, doi:10.1145/73560.73562.
  12. Donna Teague & Raymond Lister (2014): Blinded by their Plight: Tracing and the Preoperational Programmer. In: Benedict du Boulay & Judith Good: Proceedings of the 25th Annual Workshop of the Psychology of Programming Interest Group. Psychology of Programming Interest Group, pp. 8. Available at
  13. Willem Visser, Corina S. Pasareanu & Sarfraz Khurshid (2004): Test Input Generation with Java PathFinder. In: Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA '04. Association for Computing Machinery, New York, NY, USA, pp. 97–107, doi:10.1145/1007512.1007526.

Comments and questions to:
For website issues: