[pl-seminar] Talk Update (3/25/2019) - The Dilemma of Shape Analysis

[Calvin Smith <cjsmith@xxxxxxxxxxx>]

Howdy yâall,

Our schedule has changed slightly! Next Monday (3/25/2019) at 12pm in CS 4310, Thomas Reps will give a talk titled âThe Dilemma of Shape Analysisâ. The abstract follows after this message.

Sam has rescheduled his talk for the following Monday (4/1/2019) at noon, with room TBD. I will send out another email next week with the details of Samâs talk.

- Calvin

Abstract: The framework for shape analysis based on three-valued logic, developed by Sagiv, Reps, and Wilhelm, automatically creates the set of abstract transformers used for analysis from a specification of a language's concrete semantics. Each abstract transformer is constructed via a particular pattern of sub-actions, e.g., focus; coerce; check precondition; perform update action; coerce; apply abstraction.  The initial "focus; coerce" steps have been described as being a way to perform a partial concretization: the footprint of the concrete transformer is concretized, which allows the core action of the transformer to be performed in a precise fashion. The result is then abstracted.

In this talk, I will describe how the "focus; coerce" construction can be understood as essentially an independent rediscovery---but in a more general setting---of the Dilemma Rule that lies at the heart of Staalmarck's method.