Copenhagen Programming Language Seminar


Under- and over-approximation analyses using powersets and logical relations

David Schmidt,
Kansas State University, USA

Monday(!), December 6th, 15:15-16:15
DIKU, Universitetsparken 1, room N014


Almost all static analyses are overapproximating (safety) analyses, which overestimate a program's behavior in exchange for a guarantee of termination.

Overapproximating analyses can be defined in terms of Galois connections, that is, a pair of functions, $\alpha, \gamma$, where $\alpha$ defines how to map an input test-data set into an abstract value for static analysis, and $\gamma$ shows how to map the result of the analysis back to the overestimated set of outputs.

Underapproximating (liveness) analyses have gained in importance, and it is natural to try to dualize the Galois connection format, but the obvious dualization generates analyses that calculate no useful information.

This talk reviews overapproximation analysis, examines the underapproximation problem, and shows how the Galois connection framework can be applied to calculate both over- and underapproximations by using lower and upper powerdomain constructors, respectively, to construct the relevant abstract domains. Dennis Dams's under- and overapproximation analyses of state-transition systems for model checking are used as a case study.

If time allows, the role of logical relations in lifting the Galois connections to higher type and powerset type will be explained.

Scientific host: Neil Jones. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org