[pl-seminar] SAS practice talks

[Aditya Thakur <adi@xxxxxxxxxxx>]

When: 10 am, Tuesday, Sept. 4th
Where: 3310CS

Details of the two talks follow:

Title: Bilateral Algorithms for Symbolic Abstraction

Abstract:
Given a concrete domain C, a concrete operation tau: C -> C, and an
abstract domain A, a fundamental problem in abstract interpretation is
to find the best abstract transformer tau#: A -> A that
over-approximates tau.  This problem, as well as several other
operations needed by an abstract interpreter, can be reduced to the
problem of symbolic abstraction: the symbolic abstraction of a formula
phi in logic L, denoted by alphaHat(phi), is the best value in A that
over-approximates the meaning of phi.  When the concrete semantics of
tau is defined in L using a formula psi that specifies the relation
between input and output states, the best abstract transformer tau#
can be computed as alphaHat(psi).

In this paper, we present a new framework for performing symbolic
abstraction, discuss its properties, and present several
instantiations for various logics and abstract domains.  The key
innovation is to use a bilateral successive-approximation
algorithm, which maintains both an over-approximation and an
under-approximation of the desired answer.

----

Title: A Generalization of Stålmarck's Method

Abstract:
This paper gives an account of Staalmarck's method for validity
checking of propositional-logic formulas, and explains each of the key
components in terms of concepts from the field of abstract
interpretation.  We then use these insights to present a framework for
propositional-logic validity-checking algorithms that is parametrized
by an abstract domain and operations on that domain.  Staalmarck's
method is one instantiation of the framework; other instantiations
lead to new decision procedures for propositional logic.

---