How the Analyzer can Help the User Help the Analyzer

Yannick Moy

The automation offered by modern program proof tools goes hand in hand with the capability to interact with the tool when the verification fails. The SPARK proof tool tries to help…