Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Anindya Banerjee

LFCS Seminar: Anindya Banerjee

— filed under:

Modular Reasoning about Object-based Programs

  • LFCS Seminar
When Sep 05, 2012
from 11:00 AM to 12:00 PM
Where IF 3.02
Add event to calendar vCal

Shared mutable objects pose challenges in reasoning, especially for
data abstraction and modularity. We present a logic for error-avoiding
partial correctness of programs featuring shared mutable
objects. Using a first order assertion language, the logic provides
heap-local reasoning about mutation and separation, via ghost fields
and variables of type "region" (finite sets of object references).
We show how the logic can be used to reason about
hiding of internal invariants and to perform client reasoning in a manner
that does not invalidate the hidden invariants. Finally we will sketch a
derivation of program equivalence using a relational proof rule that embodies
representation independence.

Joint work with David A. Naumann and Stan Rosenberg (Stevens Institute
of Technology).

Document Actions