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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.354.4 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |