On Theorem Prover-based Testing

By Achim D. Brucker and Burkhart Wolff.

HOL-TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation.

The HOL-TestGen method is two-staged: first, the original formula 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.

Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.

Keywords:
Test Case Generation, Domain Partitioning, Test Sequence, Theorem Proving, HOL-TestGen

Please cite this work as follows:
A. D. Brucker and B. Wolff, “On theorem prover-based testing,” Formal Aspects of Computing (FAC), vol. 25, no. 5, pp. 683–721, 2013, doi: 10.1007/s00165-012-0222-y. Author copy: https://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/

BibTeX
@Article{ brucker.ea:theorem-prover:2012,
  author    = {Achim D. Brucker and Burkhart Wolff},
  journal   = {Formal Aspects of Computing (FAC) },
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  language  = {USenglish},
  title     = {On Theorem Prover-based Testing},
  year      = {2013},
  issn      = {0934-5043},
  pages     = {683--721},
  volume    = {25},
  number    = {5},
  areas     = {formal methods, software},
  doi       = {10.1007/s00165-012-0222-y},
  keywords  = {Test Case Generation, Domain Partitioning, Test Sequence,
               Theorem Proving, HOL-TestGen},
  abstract  = {HOL-TestGen is a specification and test case generation
               environment extending the interactive theorem prover
               Isabelle/HOL. As such, HOL-TestGen allows for an integrated
               workflow supporting interactive theorem proving, test case
               generation, and test data generation.
               
               The HOL-TestGen method is two-staged: first, the original
               formula 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.
               
               Due to the generality of the underlying framework, our system
               can be used for black-box unit, sequence, reactive sequence
               and white-box test scenarios. Although based on particularly
               clean theoretical foundations, the system can be applied for
               substantial case-studies.},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-theorem-prover-2012/brucker.ea-theorem-prover-2012.pdf},
}