Speaker: Greta Yorsh
Abstract: Shape analysis concerns the problem of determining ``shape invariants'' for programs that perform destructive updating on dynamically allocated storage. In recent work, it has been shown how shape analysis can be performed, using an abstract interpretation based on $3$-valued first-order logic. In that work, concrete stores are finite $2$-valued logical structures, and the sets of stores that can possibly arise during execution are represented (conservatively) using a certain family of finite $3$-valued logical structures. Current work presents results---both negative and positive---about the expressive power of $3$-valued logical structures. It also defines a non-standard (``supervaluational'') semantics for $3$-valued first-order logic that is more precise than a conventional $3$-valued semantics. Greta.