Wlp testing

tags: haskell,   tex,   11 Nov 2018

“wlp-based Automated Testing”

Abstract - In this paper we describe our process and solution for creating a wlp-based automated testing tool for the GCL language given in (“Project: wlp-based Automated Testing” 2018). First, we describe how we can represent the GCL programs as instances of our internal datatypes. Afterwards, the generation of paths is discussed, along with a solution to the infinite-while paths problem. After this, generating a WLP based on these found paths is discussed. This WLP will then be translated to a DNF in order to function as the input for our solve function that tries to find counter examples for the given propositions. Finally, the addition of program calls is discussed, along with how to inline these calls and deal with the problem of shadowing variables.

GitHub repository (access on request)
CS Course: Program Semantics and Verification

Disclaimer: The above content and related documentation, papers, essays, code and other references, were created during a course of the MSc Computing Science. No rights can be derived from the content. Much work has been done in collaboration with other students. If there is any reference to your person in any way that you would like to see removed or to be named (more) explicitly, at any time, please let me know.