Practical Techniques for Auto-Active Verification
Event details
| Date | 16.07.2014 |
| Hour | 14:15 |
| Speaker | Nadia Polikarpova |
| Location | |
| Category | Conferences - Seminars |
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.
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.
Practical information
- Informed public
- Free