University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Practical Techniques for Auto-Active Verification

Practical Techniques for Auto-Active Verification

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity