Practical Techniques for Auto-Active Verification

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

• Nadia Polikarpova
• Tuesday 08 July 2014, 11:00-12:00
• Room 217, Department of Computing.

If you have a question about this talk, please contact George A Constantinides.

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.

Bio:

Nadia Polikarpova obtained her PhD at ETH Zurich in April 2014. Her research interests lie in the area of software correctness, at the intersection of formal methods and software engineering. In particular, her research has contributed to auto-active verification, behavioral interface specifications, automated testing, dynamic invariant inference, and user interface for verification.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• Room 217, Department of Computing

Note that ex-directory lists are not shown.