The formal, mechanized, verification of computer programs is a particularly difficult task in fast-evolving and complex development environments, as it typically is a slow process. To speed things up, verification efforts often target abstract models of these programs, and many implementation details are often left unverified in critical code. In this blog post, we propose to bridge the verification gap between a mechanized model and its implementation by leveraging property-based testing. Co...
