Automatic testing of programming assignments is highly desirable as it can provide fast feedback for the students and allows the teachers to teach efficiently even in courses with many students. However, writing tests for students' solutions can be tedious. In this work, we present a novel approach to test generation for small Haskell assignments. Such assignments usually consist of one function (with the possibility to use helper functions in its definition) that the students are supposed to program according to a teacher's specification. The teacher is not required to write tests for this function. Instead, we make use of an example solution, which the teacher should have to assess the difficulty of the assignment. Using the example solution, and (if needed) a specification of input values for the function, our tool can automatically generate randomized tests. If these tests fail, the student is presented with a counterexample which shows the input values, the expected output of the tested function and the output computed by their solution.

DIVINE is an LLVM -based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE , it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.

An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language. Our implementation consists of 2 parts: an implementation of the 'libunwind' platform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions.