# AutoProof: Auto-active Functional Verification of Object-oriented Programs

arXiv: https://arxiv.org/abs/1501.03063 · HTML: https://mlsanity.com/paper/1501.03063/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jan 2015.

## Built on by (most cited first, 1 of 1)

- [Do AI models help produce verified bug fixes?](https://mlsanity.com/paper/2507.15822/) (2025)

## Abstract (arXiv)

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.