Abstract

Auto-active verification occupies a niche between fully automatic analysis and interactive proofs: it targets a high degree of automation (usually powered by SMT solvers), while supporting programmer-friendly user interaction through source code annotations. This talk will describe a practical auto-active approach to verifying object-oriented programs and discuss techniques for making users’ interaction with auto-active tools more effective.

Invariant-based reasoning about object-oriented programs becomes challenging in the presence of collaborating objects that need to maintain global consistency. This talk will present semantic collaboration: a methodology to specify and reason about class invariants that models dependencies between collaborating objects by semantic means. The methodology is implemented in an auto-active verifier for the Eiffel programming language, and evaluated on several challenge problems and a realistic data structure library.

One of the biggest remaining obstacles to using auto-active verifiers in practice is the quality of feedback they provide when a proof attempt fails. The second part of the talk will describe a technique to generate concrete test cases for programs annotated with complex specifications, which helps understand and debug failed verification attempts.