IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2010 > Local reasoning for Java programs and its automation
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Stan Rosenberg

lunes 25 de enero de 2010

3:15pm Amphitheatre H-1002

Stan Rosenberg, PhD candidate, Stevens Institute of Technology, Hoboken, USA

Local reasoning for Java programs and its automation


Shared mutable objects are a cornerstone of the object-oriented paradigm. Modular reasoning remains a challenge. For example, how can a client of setLeftZero be certain that the right subtree did not change after the invocation?

In this talk, I will describe a program logic, called Region Logic, designed to control aliasing through explicit use of effects and disjointness assertions. The logic employs regions (sets of references) in a novel way, by using them in ghost state (i.e., as program annotations), effects and assertions. The region assertion language is especially instrumental in reasoning about many interesting “lightweight” specifications (e.g., without reachability predicates or inductive definitions).

To substantiate the preceding claim, I will present a specification (in Region Logic) derived from the Composite design pattern challenge problem and describe how to automatically verify it. Lastly, I will give some insight into a decision procedure for quantifier-free region assertions.