Grading and giving feedback to student submissions automatically is becoming more and more necessary with an increasing amount of students. To verify the correctness of student-written definitional interpreters, a program equivalence approach has been implemented, improved, and extended with new rules to make it more suited specifically for verifying interpreters. This approach is able to soundly recognise two different interpreters as equivalent. Interpreters can thus be compared to a correct interpreter to verify their correctness or be grouped with equivalent interpreters to be graded in batches. Using program equivalence in combination with other verification approaches can improve the process of giving feedback to students and help build up a collection of common errors made by students.

Definitional interpreters are difficult to test with a pre-defined test suite. This paper tries to determine the effectiveness of automatic testing of definitional interpreters, using concolic execution. First we develop a model for concolic execution of a functional language. Then we identify different categories of common mistakes when writing interpreters and test which are caught by concolic execution. We find that while concolic execution is promising, as it can find counterexamples for most errors in a small language, the model developed in this paper is not sufficient to generate counterexamples for more complicated languages.