Automated Instantiation of Control Flow Tracing Exercises

Clemens Eisenhofer
(TU Wien)
Martin Riener
(TU Wien)

One of the first steps in learning how to program is reading and tracing existing code. In order to avoid the error-prone task of generating variations of a tracing exercise, our tool Tatsu generates instances of a given code skeleton automatically. This is achieved by a finite unwinding of the program in the style of bounded model checking and using the SMT solver Z3 to find models for this unwinded program.

In João Marcos, Walther Neuper and Pedro Quaresma: Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (ThEdu'21), (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021, Electronic Proceedings in Theoretical Computer Science 354, pp. 43–58.
Published: 8th February 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: