IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2011 > A Lower Bound on Resource Verification
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Alexander Malkis

martes 17 de mayo de 2011

11:00am Meeting room 302 (Mountain View), level 3

Alexander Malkis, Post-doctoral Researcher, IMDEA Software Institute

A Lower Bound on Resource Verification

Abstract:

In multi-threaded programs data is often separated into lock-protected resources. Properties of those resources are typically verified by modular, Owicki-Gries-like methods. The Owicki-Gries proof structure follows the program syntax in an intuitive, cheap and easily implementable and extendable manner (Concurrent Separation Logic, Chalice, VCC, RGSep, …). Alas, some properties do not admit this proof structure. So far nothing was known about the boundary between properties that do have this proof structure and properties that don’t have it. We will characterize a class of properties that do admit an Owicki-Gries proof structure, showing what properties are always cheaply provable and a worst-case approximation inherent to the Owicki-Gries method.