Automated Instantiation of Control Flow Tracing Exercises

TL;DR

This paper introduces Tatsu, a tool that automatically generates variations of control flow tracing exercises by unwinding code and using SMT solving, aiding programming education.

Contribution

It presents a novel method combining bounded model checking and SMT solving to automatically instantiate control flow tracing exercises from code skeletons.

Findings

Successfully generates diverse tracing exercises

Reduces manual effort in creating programming practice problems

Demonstrates effectiveness with real code examples

Abstract

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.