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.
@article{arxiv.2202.03565,
title = {Automated Instantiation of Control Flow Tracing Exercises},
author = {Clemens Eisenhofer and Martin Riener},
journal= {arXiv preprint arXiv:2202.03565},
year = {2022}
}