Practical Techniques for Auto-Active Verification

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

• Dr Nadia Polikarpova, ETH Zurich
• Tuesday 08 July 2014, 11:00-12:00
• Room 503, EEE.

If you have a question about this talk, please contact Wiesia R Hsissen.

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 practical auto-active verification techniques in two problem domains: heap-manipulating object-oriented programs and implementations of security protocols. 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, which 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 programs and a realistic data structure library. The second part of the talk will describe a technique for verifying high-level security properties of cryptographic protocol implementations within an auto-active program verifier for C. The technique is based on stepwise refinement, and has been used to verify parts of Microsoft’s Trusted Platform Module.

This talk is part of the Circuits and Systems Group: Internal Seminars series.

This talk is included in these lists:

• Circuits and Systems Group: Internal Seminars
• Room 503, EEE

Note that ex-directory lists are not shown.