Lightweight Interactive Proving inside an Automatic Program Verifier

Sylvain Dailler, Claude Marché, Yannick Moy

Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of hu…