Skip to main content

One post tagged with "property based testing"

View All Tags

ยท 7 min read
Guillaume Claret

Property based tests are a way to find bugs in the code by running a boolean function (representing an expected property) on randomly generated inputs. In this blog post, we show how we translate these tests to corresponding Coq theorems. Once we have a formal representation, we prove them correct on any inputs. Thanks to this technique, we can:

  • have a bridge between the specification given by the tests and the specification in Coq;
  • make sure that the properties verified in the tests are true with a mathematical degree of certainty.

We have done this work with students from the University of Groningen: