TY - JOUR AU - Brucker, Achim D. AU - Brügger, Lukas AU - Wolff, Burkhart PY - 2008 DA - 2008// TI - Verifying Test-Hypotheses: An Experiment in Test and Proof JO - Electronic Notes in Theoretical Computer Science SP - 15 EP - 27 VL - 220 IS - 1 PB - Elsevier Science Publishers CY - Amsterdam KW - symbolic test case generations, black box testing, theorem proving, formal verification, Isabelle/HOL AB - HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. The HOL-TestGen method is two-staged: first, the original formula, called test specification, is partitioned into test cases by transformation into a normal form called test theorem. Second, the test cases are analyzed for ground instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test hypotheses which can be proven over concrete programs. As such, explicit test hypotheses establish a logical link between validation by test and by proof. Since HOL-TestGen generates explicit test hypotheses and makes them amenable to formal proof, the system is in a unique position to explore the relations between them at an example. SN - 1571-0661 L1 - https://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008 UR - https://doi.org/10.1016/j.entcs.2008.11.003 DO - 10.1016/j.entcs.2008.11.003 LA - USenglish N1 - Proceedings of the Fourth Workshop on Model Based Testing (MBT 2008) ID - brucker.ea:verifying:2008 ER -