Practical Techniques for Auto-Active Verification

Add to your list(s) Download to your calendar using vCal

• Nadia Polikarpova, ETH Zurich
• Wednesday 09 July 2014, 11:00-12:00
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.