CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

AutoProof: auto-active functional verification of object-oriented programs

Carlo A. Furia (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; M. Nordio ; N. Polikarpova ; J. Tschannen
International Journal on Software Tools for Technology Transfer (1433-2779). p. 1-20. (2016)
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: Auto-active verification , Functional verification , Object-oriented verification , Verification benchmarks



Denna post skapades 2017-01-16.
CPL Pubid: 247118

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur