Steps toward usable verification

Опубликовано 21 июня 2016, 21:17

First, I will provide some background information on CodeContracts, the language-agnostic specification language of .NET 4.x, and on Clousot, the companion abstract interpretation-based verifier. I will explain why we chose abstract interpretation instead of, e.g., using a theorem prover and discuss our experience with its adoption both inside and outside the company. Then, I will cover topics that make the verification usable by the working programmers: inference of necessary preconditions, verified code repairs, refactoring with contracts, and verification modulo versions. En passant, I will present a generalization of Hoare Logic, Algebraic Hoare Logic, and show how the usual conjunction and disjunction rules require extra hypotheses to ensure soundness.