Copenhagen Programming Language Seminar


Comparing completeness properties of static analyses and their logics

David Schmidt,
Kansas State University, USA

Tuesday (!), February 27, 15:15-16:00
DIKU, Universitetsparken 1, Room N034


Static analyses calculate abstract states, and their logics validate properties of the abstract states. We place into perspective the variety of forwards, backwards, functional, and logical completeness used in abstract-interpretation-based static analysis by giving examples and by proving equivalences, implications, and independences. We expose two fundamental Galois connections that underlie the logics for static analyses and reveal a new completeness variant, O-completeness. We also show that the key concept underlying logical completeness is covering, which we use to relate the various forms of completeness.

Scientific host: Andrzej Filinski. Administrative host: Camilla Torp-smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
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