Auto active verification

[Google Scholar]

Notes: Boogie verifier, Dafny verifier, VeriFast verifier
Papers: nelson:sosp:2019

A term coined by Leino and Moskal

[…] all interaction with the program verifier [is] done with annotations supplied in the program text […]. This was made possible by powerful automatic satisfiability-modulo-theories (SMT) solvers.
— Usable auto-active verification, Usable Verification Workshop 2010.

though I think they are retroactively naming what the ESC report did.

A more recent description

In contrast to interactive theorem provers, auto-active theorem provers ask developers to write proof annotations on implementation code, such as preconditions, postconditions, and loop invariants. The prover translates the annotated code into a verificationcondition and invokes a constraint solver to check its validity.
— nelson:sosp:2019

Some examples are the Dafny verifier, the Boogie verifier and the VeriFast verifier.

Annotation burden, Dafny verifier, VCC verifier