AutoProof: Auto-Active Functional Verification of Object-Oriented Programs
Julian Tschannen, Carlo A. Furia, Martín Nordio, Nadia Polikarpova · 2015
Abstract. Auto-active verifiers provide a level of automation intermediate be-tween fully automatic and interactive: users supply code with annotations as in-put 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 se-quential programs with complex functional specifications. AutoProof fully sup-ports 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, de-sign, and implementation features, and demonstrates AutoProof’s performance on a rich collection of benchmark problems. The results attest AutoProof’s com-petitiveness among tools in its league on cutting-edge functional verification of object-oriented programs. 1 Auto-active Functional Verification of Object-oriented Programs Program verification techniques differ wildly in their degree of automation and, cor-respondingly, in the kinds of properties they target. One class of approaches—which