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.
Some examples are the Dafny verifier, the Boogie verifier and the VeriFast verifier.
Notes related to Auto active verification
Annotation burden, Dafny verifier, VCC verifier
Papers related to Auto active verification
- VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
- VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
- Developing verified programs with Dafny [leino:icse:2013]
- Extended static checking: A ten-year perspective [leino:informatics:2001]
- Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
- Annotation inference for separation logic based verifiers [vogels:fmoods:2011]