Automated Instantiation of Control Flow Tracing Exercises

Eisenhofer, Clemens; Riener, Martin

doi:10.4204/EPTCS.354.4

Record link:

http://hdl.handle.net/20.500.12708/175702

Title:

Automated Instantiation of Control Flow Tracing Exercises

Citation:

Eisenhofer, C., & Riener, M. (2022). Automated Instantiation of Control Flow Tracing Exercises. In J. Marcos, W. Neuper, & P. Quaresma (Eds.), Proceedings 10th International Workshop on Theorem Proving Components for Educational Software (pp. 43–58). EPTCS. https://doi.org/10.4204/EPTCS.354.4

CatalogPlus:

AC17202065

Publisher DOI:

10.4204/EPTCS.354.4

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Eisenhofer, Clemens
Riener, Martin

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering
E192-05 - Forschungsbereich Theory and Logic

Published in:

Proceedings 10th International Workshop on Theorem Proving Components for Educational Software

Volume:

354

DOI of the book:

10.4204/EPTCS.354

Date (published):

8-Feb-2022

Event name:

10th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2021

Event date:

11-Jul-2021

Event place:

Pittsburgh, United States of America (the)

Number of Pages:

Publisher:

EPTCS

Keywords:

Education; Tracing; Exercise Generation; Satisfiability Modulo Theories; Bounded Model Checking

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.

Research Areas:

Mathematical and Algorithmic Foundations: 80%
Computational System Design: 20%

Science Branch:

1020 - Informatik: 100%

License:

CC BY-SA 4.0