| 1 Mission Theorem-prover based Testing with HOL-TestGen (Extended Abstract) (2009) | |||||||||||||||
Abstract | |||||||||||||||
| and software testing. As far as symbolic verification methods and modelbased testing techniques are concerned, the interest among researchers in the mutual fertilization of these fields is growing. From the verification perspective, testing offers: – experiences on test-adequacy criteria [6], which can be viewed as new abstraction techniques reducing infinite models to finite and checkable ones, – new approaches to generate counter-examples, and – new application scenarios for verification, since black-box testing can be used as a systematic experimentation method for reverse engineering specifications for legacy systems. From the testing perspective, symbolic verification offers: – ways to cope with the state space explosions inherent to test case generation techniques, and – ways to log the testing hypothesis underlying a test explicitly. The hol-TestGen system [3,2,1] is designed to explore and exploit these | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||