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.
Notes related to Auto active verification
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]