BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Practical Techniques for Auto-Active Verification
DTSTART:20140716T141500
DTSTAMP:20260407T051317Z
UID:01e5e103f03931a20b8b00e32ebb0cb4ccd2966811392541b86a28bf
CATEGORIES:Conferences - Seminars
DESCRIPTION:Nadia Polikarpova\nAuto-active verification occupies a niche b
 etween fully automatic analysis and interactive proofs: it targets a high 
 degree of automation (usually powered by SMT solvers)\, while supporting p
 rogrammer-friendly user interaction through source code annotations. This 
 talk will describe a practical auto-active approach to verifying object-or
 iented programs and discuss techniques for making users' interaction with 
 auto-active tools more effective.\nInvariant-based reasoning about object-
 oriented programs becomes challenging in the presence of collaborating obj
 ects that need to maintain global consistency. This talk will present sema
 ntic collaboration: a methodology to specify and reason about class invari
 ants that models dependencies between collaborating objects by semantic me
 ans. The methodology is implemented in an auto-active verifier for the Eif
 fel programming language\, and evaluated on several challenge problems and
  a realistic data structure library.\nOne of the biggest remaining obstacl
 es to using auto-active verifiers in practice is the quality of feedback t
 hey provide when a proof attempt fails. The second part of the talk will d
 escribe a technique to generate concrete test cases for programs annotated
  with complex specifications\, which helps understand and debug failed ver
 ification attempts.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR