Test Execution Framework in HOL-TestGen

Description

[HOL-TestGen](ch/projects/hol-testgen/) is a specification-based test case generation environment. While HOL-TestGen allows to generate test cases, it currently lacks a state of the art framework for executing tests as well as monitoring and analysing the test runs.

In this project, a generic test execution and reporting framework (e.g., similar to the core of [JUnit](org) but instead of writing test cases manually, they are automatically generated by HOL-TestGen) for [HOL-TestGen](ch/projects/hol-testgen/) will be developed that supports various test scenarios (e.g., unit tests, sequence tests) as well as implementation technologies.

Usually, either a significant (non-trivial) programming task or a signifiant theoretical contribution are expected to make up a suitable project.

Skills required:

• Good programming skills
• An interest in functional programming (e.g, SML, Ocaml, Haskell)
• An interest in testing
• An interest in formal methods and/or theorem proving (e.g., Isabelle/HOL)

Initial reading and useful links:

• JUnit: <org>