A generator of test-data from HOL specifications

Project funded by Univ. P-Sud
The ultimate goal of this research project is to extend the realm of feasible state-spaces for HOL-TestGen system (see by 4 orders of magnitude - thus offering even more potential for industrial applications in realistic model-based test-scenarios. We suggest a combination of 3 techniques to achieve this goal:
- We will combine HOL-TestGen with reasonably integrated and configured automated provers from the SAT solver system family, in particular Z3.
- With increasing complexity, there will always remain unresolvable constraints. We will use new Isabelle code-generators to convert constraint-systems of unknown logical status into optimized random test code.
- In our experience, the success depends substantially on
derived rules from the test domain that help to detect unsatisfiable test-cases early. We will explore ways to derive such forms of domain-specific simplification rules can be automated.

Research activities
  SAT
  Verification
  Software Testing
  Higher-Order Languages
  Formal Methods for Software Engineering

Participants
WOLFF Burkhart


More information : http://www.lri.fr/~wolff/research.html#section1b