Tests from failed proofs

Potential supervisors: 

When an automatic static proof of correctness fails, it typically fails in some specific cases. The failing cases correspond to preconditions for which the prover could not guarantee that the program behaves as in its specification. However, this does not necessarily mean that the program has a bug; in many cases, a proof fails simply because it requires more detailed intermediate annotations (for example, a better loop invariant). In these cases, it is helpful to complement static proofs with testing, which may find concrete bugs -- if they exist -- or confirm that the program works correctly for a variety of concrete inputs.

In this project, you will implement a technique to build tests from failed proofs. We will target the language Java, and use the static prover KeY, which is capable of isolating preconditions corresponding to partially failed proofs, in combination with test-case generation tools for Java such as EvoSuite or Randoop.

Related courses:

  • Testing, debugging and verification
  • Formal methods for software development

Reading and resources:

  1. The KeY prover: https://www.key-project.org/
  2. The test-case generation tools EvoSuite http://evosuite.org/ and Randoop https://randoop.github.io/randoop/
  3. A description of how the KeY tool is used in the context of combined static and runtime verification: https://link.springer.com/article/10.1007/s10703-017-0274-y

Contact: Gerardo Schneider (gersch@chalmers.se)

Date range: 
October, 2017 to October, 2022