Approximating Module Semantics with Constraints

Abstract:

In this paper we present a generic constraint domain for symbolic modular analysis. The idea is that the semantics of a module can be approximated by a set of relations symbolically linking the input, output and local variables. We show how this result is correct w.r.t. a trace semantics, and how it can be used to perform an (incremental) modular analysis. We claim that our construction generalizes existing modular analyses by showing how well-known modular analyses can be instantiated in our framework.

Back to the Homepage