AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

This talk presents connections between logic and abstract
interpretation. In particular, I will present a new algorithm for the
problem of "symbolic abstraction": Given a formula \phi in a logic L
and an abstract domain A, the symbolic abstraction of \phi is the best
abstract value in A that over-approximates the meaning of \phi. When
\phi represents a concrete transformer, algorithms for symbolic
abstraction can be used to automatically synthesize the corresponding
abstract transformer. Furthermore, if the symbolic abstraction of
\phi is bottom, then \phi is proved unsatisfiable.

The bottom line is that our algorithm is "dual-use": (i) it can be
used by an abstract interpreter to compute abstract transformers, and
(ii) it can be used in an SMT (Satisfiability Modulo Theories) solver
to determine whether a formula is satisfiable.

The key insight behind the algorithm is that Staalmarck's method for
satisfiability checking of propositional-logic formulas can be
explained using concepts from the field of abstract interpretation.
This insight then led to the discovery of the connection between
Staalmarck's method and symbolic abstraction, and the extension of
Staalmarck's method to richer logics, such as quantifier-free linear
real arithmetic.
This is joint work with Prof. Thomas Reps.

Rupak Majumdar

0631-9303-8500

--email hidden

Yes

Saarbrücken

E1 5

029

passcode not visible

logged in users only