Program-based test-generation methods (also called “white-box” tests) are conventionally described in terms of a control flow graph and the generation of path conditions along the paths in this graph. In this paper, we present an alternative formalization based on state-exception monads that allows for direct derivations of path conditions from program presentations in them; the approach lends itself both for program-based testing procedures—designed to meet classical coverage criteria—and bounded verification. Our formalization is implemented in the Isabelle/HOL interactive theorem prover, where symbolic execution can be processed through tactics implementing test-generation strategies for various coverage criteria. The resulting environment is a major step towards testing support for the development of invariants and post-conditions in C verification environments similar to Isabelle/AutoCorres.
CITATION STYLE
Keller, C. (2018). Tactic program-based testing and bounded verification in isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10889 LNCS, pp. 103–119). Springer Verlag. https://doi.org/10.1007/978-3-319-92994-1_6
Mendeley helps you to discover research relevant for your work.