Genetic algorithm with temporal logic for automated markers

Abstract

Automated assessment is essential for large-scale programming courses, as it addresses the challenges of evaluating correctness and providing feedback efficiently. Traditional methods of automated assessment rely on hand-crafted test cases, which are time-intensive and lack scalability. Automated test generation methods, such as random input generation or genetic algorithms combined with code coverage metrics, offer alternatives, but often fail to capture the complexity required for educational assessments. To address this, a novel approach that integrates genetic algorithms with linear temporal logic (LTL) formulae is proposed. LTL properties, commonly used in model checking, formalise correctness criteria for programming assignments. The proposed method evolves test cases designed to maximise violations of the LTL properties in student submissions, determining correctness and generating personalised feedback by providing examples of failing test cases. Experiments \replaced{were}{are} conducted to evaluate the approach in terms of sensitivity to hyperparameter settings, and effectiveness relative to the established techniques, such as random input generation and code coverage-based genetic algorithms. Results demonstrate that combining genetic algorithms with LTL properties enhances automated assessment accuracy and feedback quality, offering a solution to the problems faced by automated assessment in large educational settings for both students and lecturers.