AutoProof swMATH ID: 30948 Software Authors: Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N. Description: AutoProof: Auto-active Functional Verification of Object-oriented Programs. 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. Homepage: http://se.inf.ethz.ch/research/autoproof/ Source Code: https://github.com/julian-tschannen/autoproof Keywords: Logic; arXiv_cs.LO; Auto-active verifiers; Functional Verification; Object-oriented Programs; AutoProof Related Software: Dafny; VCC; Spec#; Why3; KeY; VeriFast; Eiffel; z3; OpenJML; Boogie; JML; Viper; BVD; ESC/Java; WhyML; Coq; Rodin; TraitRecordJ; TraitCbC; Featherweight Java Cited in: 6 Publications Standard Articles 1 Publication describing the Software Year AutoProof: Auto-active Functional Verification of Object-oriented Programs Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N. 2015 all top 5 Cited by 22 Authors 1 Brenas, Jon Haël 1 Bubel, Richard 1 Chechik, Marsha 1 de Boer, Frank S. 1 De Gouw, Stijn 1 Echahed, Rachid 1 Ghezzi, Carlo 1 Groves, Lindsay J. 1 Hähnle, Reiner 1 Leino, K. Rustan M. 1 Lucio, Paqui 1 Menghi, Claudio 1 Pearce, David J. 1 Potanin, Alex 1 Rot, Jurriaan 1 Runge, Tobias 1 Schaefer, Ina 1 Spoletini, Paola 1 Steinhöfel, Dominic 1 Strecker, Martin 1 Thüm, Thomas 1 Utting, Mark Cited in 3 Serials 2 Journal of Automated Reasoning 1 Formal Aspects of Computing 1 ACM Transactions on Computational Logic Cited in 2 Fields 6 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year