Sökning: onr:"swepub:oai:research.chalmers.se:7206e750-00f6-425c-9766-dfeed94bac56" >
AutoProof: auto-act...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Verification benchmarks
- Functional verification
- Object-oriented verification
- Auto-active verification
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas