Auto-active verifiers provide a level of automation intermediate between
fully automatic and interactive: users supply code with annotations as input
while benefiting from a high level of automation in the back-end. This paper
presents AutoProof, a state-of-the-art auto-active verifier for object-oriented
sequential programs with complex functional specifications. AutoProof fully
supports advanced object-oriented features and a powerful methodology for
framing and class invariants, which make it applicable in practice to idiomatic
object-oriented patterns. The paper focuses on describing AutoProof's
interface, design, and implementation features, and demonstrates AutoProof's
performance on a rich collection of benchmark problems. The results attest
AutoProof's competitiveness among tools in its league on cutting-edge
functional verification of object-oriented programs.