[PRL] Fwd: [MIT-PL] Fwd: Fwd: Nov 24, 11:00 -12:30 - Guest Speaker: Anindya Banerjee, NSF

[Phillip Mates]

Anindya Banerjee is giving an interesting looking talk at BU (~20 min walk)
next Monday.

---------- Forwarded message ----------
From: Adam Chlipala <adamc at csail.mit.edu>
Date: Wed, Nov 19, 2014 at 2:38 PM
Subject: [MIT-PL] Fwd: Fwd: Nov 24, 11:00 -12:30 - Guest Speaker: Anindya
Banerjee, NSF
To: pl at csail.mit.edu





-------- Forwarded Message --------  Subject: Fwd: Nov 24, 11:00 -12:30 -
Guest Speaker: Anindya Banerjee, NSF  Date: Wed, 19 Nov 2014 11:29:26
-0500  From:
Assaf Kfoury <kfoury at bu.edu> <kfoury at bu.edu>  To: adamc at csail.mit.edu

  Hello Adam:

 I hope this email finds you well. I write to let you know about a talk by
Anindya Banerjee on Monday, November 24, at 11 am (see below). I hope you
(and anyone else around you interested in PL foundations) can make it.

 Best,
   Assaf

   ---------- Forwarded message ----------
From: Hariri Institute for Computing <hicadmin at bu.edu>
Date: Tue, Nov 18, 2014 at 2:00 PM
Subject: Nov 24, 11:00 -12:30 - Guest Speaker: Anindya Banerjee, NSF
To: kfoury at bu.edu


       Wednesdays @Hariri Announcement
  View it in your browser
<http://us6.campaign-archive2.com/?u=e3ad8f42733d54531fb729327&id=bf273812b4&e=74122e47ba>
         [image: Rafik B. Hariri Institute for Computing and Computational
Science & Engineering]
<http://www.us6.list-manage.com/track/click?u=e3ad8f42733d54531fb729327&id=4c4727ca33&e=74122e47ba>
         *Guest Speaker: Anindya Banerjee*
Program Director
CCF Division of the CISE Directorate
National Science Foundation


Modular Reasoning for Behavior-Preserving Data Structure Refactorings

11:00 AM on November 24, 2014 @MCS-180
------------------------------

*Abstract: *A properly encapsulated data structure can be revised for
refactoring without affecting the behaviors of clients of the
data structure. Encapsulation ensures that clients are
"representation independent", that is, they are independent of particular
choices of data structure representations. Modular reasoning about data
structure revisions in heap-manipulating programs, however, is a
challenge because encapsulation in the presence of shared mutable objects
is difficult to ensure for a variety of reasons:

(a) Pointer aliasing can break encapsulation and invalidate data structure
invariants.

(b) Representation independence (RI) is nontrivial to guarantee in
a generic manner, without recourse to specialized disciplines such
as ownership.

(c) Mechanical verification of RI using theorem provers is nontrivial
because it requires relational reasoning between two different data
structure representations. Such reasoning lies outside the scope of most
modern verification tools.

We address the challenges by reasoning in Region Logic (RL), a Hoare logic
augmented with state dependent “modifies” specifications based
on simple notations for object sets, termed "regions". RL uses ordinary
first order logic assertions to support local reasoning and also the hiding
of invariants on encapsulated state, in ways suited to verification using
SMT solvers. By using relational assertions, the logic can reason about
behavior-preservation of data structure refactorings even in settings where
full functional pre/post specifications are absent. The key ingredient
behind such reasoning is a new proof rule that embodies representation
independence.

A verifier based on the non-relational part of RL has been used in
the verification of implementations of the Observer and Composite design
patterns and their clients. We further expect RL to be useful in proving
noninterference style properties in the context of information flow
security.

Work in progress with David A. Naumann and Mohammad Nikouei
(Stevens Institute of Technology).

*Bio: *Anindya Banerjee is currently Program Director in the CCF Division
of the CISE Directorate at the National Science Foundation, where he
participates in the Software and Hardware Foundations (SHF), REU Sites, and
Cyberphysical Systems (CPS) programs and leads the Exploiting Parallelism
and Scalability (XPS) program. He is on leave from the IMDEA Software
Institute, Madrid, Spain, where he is full professor. Anindya's research
spans: Programming languages and program verification; High assurance
concurrent, distributed and networked systems; Cyber-security, specifically
the modular verification and certification of software systems against
security policies; Program logics and semantics; Program analysis and
abstract interpretation.


 ------------------------------

*To schedule or suggest a talk for future meetings, please send us an email
at hicadmin at bu.edu <hicadmin at bu.edu>. *
           Forward to a friend
<http://us6.forward-to-friend.com/forward?u=e3ad8f42733d54531fb729327&id=bf273812b4&e=74122e47ba>

  *Copyright © 2014 Boston University, All rights reserved.*
This email is courtesy of the Hariri Institute for Computing.
*Our mailing address is:*
Boston University
111 Cummington Mall
Boston, MA 02215

Add us to your address book
<http://www.us6.list-manage.com/vcard?u=e3ad8f42733d54531fb729327&id=b80d62cea1>
  [image: Email Marketing Powered by MailChimp]
<http://www.mailchimp.com/monkey-rewards/?utm_source=freemium_newsletter&utm_medium=email&utm_campaign=monkey_rewards&aid=e3ad8f42733d54531fb729327&afl=1>
    unsubscribe from this list
<http://www.us6.list-manage.com/unsubscribe?u=e3ad8f42733d54531fb729327&id=b80d62cea1&e=74122e47ba&c=bf273812b4>
| update subscription preferences
<http://www.us6.list-manage.com/profile?u=e3ad8f42733d54531fb729327&id=b80d62cea1&e=74122e47ba>






_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl
-------------- next part --------------
HTML attachment scrubbed and removed