Theorem-prover based Testing with HOL-TestGen

Theorem-prover based Testing
with HOL-TestGen
1 2 3Achim D. Brucker Lukas Brügger Burkhart Wolff
1SAP Research, Vincenz-Priessnitz-Str. 1, 76131 Karlsruhe, Germany
achim.brucker@sap.com
2Information Security, ETH Zürich, Switzerland
lukas.bruegger@inf.ethz.ch
3Universität des Saarlandes, 66041 Saarbrücken, Germany
wolff@wjpserver.cs.uni-sb.de
A Tutorial at NII
Tokyo, 9th June 2008Outline
1 Motivation and Introduction
2 From Foundations to Pragmatics
3 Advanced Test Scenarios
4 Case Studies
5 ConclusionOutline
1 Motivation and Introduction
2 From Foundations to Pragmatics
3 Advanced Test Scenarios
4 Case Studies
5 ConclusionMotivation and Introduction Motivation
State of the Art
“Dijkstra’s Verdict”:
Program testing can be used to show the presence of bugs, but
never to show their absence.
Is this always true?
Can we bother?
A.D. Brucker and L. Brügger and B. Wolff HOL-TestGen: Theorem-prover based Testing A Tutorial at NII 4Motivation and Introduction Motivation
Our First Vision
Testing and verification may converge,
in a precise technical sense:
specification-based (black-box) unit testing
generation and management of formal test hypothesis
verification of test hypothesis (not discussed here)
A.D. Brucker and L. Brügger and B. Wolff HOL-TestGen: Theorem-prover based Testing A Tutorial at NII 5Motivation and Introduction Motivation
Our Second Vision
Observation:
Any testcase-generation technique is based on and limited
by underlying constraint-solution techniques ...