text: In this paper we promote introducing software verification and control flow graph similarity measurement in automated evaluation of students' programs. We present a new grading framework that merges results obtained by combination of these two approaches with results obtained by automated testing, leading to improved quality and precision of automated grading. These two approaches are also useful in providing a comprehensible feedback that can help students to improve the quality of their programs We also present our corresponding tools that are publicly available and open source. The tools are based on LLVM low-level intermediate code representation, so they could be applied to a number of programming languages. Experimental evaluation of the proposed grading framework is performed on a corpus of university students' programs written in programming language C. Results of the experiments show that automatically generated grades are highly correlated with manually determined grades suggesting that the presented tools can find real-world applications in studying and grading.
  @cite_35: 
  @cite_34: This paper presents the Open CAEsar software architecture, which allows to integrate in a common framework different languages formalisms for the description of concurrent systems, as well as tools with various functionalities, such as random execution, interactive simulation, on-the-fly and exhaustive verification, test generation, etc. These principles have been fully implemented, leading to an open, extensible, and well-documented programming environment, which allows tools to be developed in a modular framework, independently from any particular description language.
  @cite_26: We present design and evaluation of LAV, a new open-source tool for statically checking program assertions and errors. LAV integrates into the popular LLVM infrastructure for compilation and analysis. LAV uses symbolic execution to construct a first-order logic formula that models the behavior of each basic blocks. It models the relationships between basic blocks using propositional formulas. By combining these two kinds of formulas LAV generates polynomial-sized verification conditions for loop-free code. It uses underapproximating or overapproximating unrolling to handle loops. LAV can pass generated verification conditions to one of the several SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments with small 200 benchmarks suggest that LAV is competitive with related tools, so it can be used as an effective alternative for certain verification tasks. The experience also shows that LAV provides significant help in analyzing student programs and providing feedback to students in everyday university practice.
summary: Software verification techniques are not commonly used in automated evaluation of programs. There are limited experiments on using Java PathFinder model checker for automated test case generation @cite_35 . Tools with integrated support for automated testing and verification, e.g. Ceasar @cite_34 , are usually too complex and not aimed for educational purposes. To the authors' knowledge, there is no other software verification tool deployed in process of automated bug finding as a complement to automated testing of students' programs. The tool LAV was already used, to a limited extent, for finding bugs in students' programs @cite_26 . In that work, a different sort of corpus was used, as discussed in Section . Also, that application did not aim at automated grading, and instead was made in the wider context of design and development of LAV as a general-purpose SMT-based error finding platform.