论文标题
控制流跟踪练习的自动实例化
Automated Instantiation of Control Flow Tracing Exercises
论文作者
论文摘要
学习如何编程的第一步之一是读取和追踪现有代码。为了避免容易产生跟踪练习的变化的任务，我们的工具TATSU会自动生成给定代码骨架的实例。这是通过以有限的模型检查风格的有限放松程序来实现的，并使用SMT求解器Z3来找到此不受欢迎的程序的模型。
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.
