Logical approximation for program analysis

The abstract interpretation of programs relates the exact semantics of a programming language to an approximate semantics that can be effectively computed. We show that, by specifying operational semantics in a specification framework based on bottom-up logic programming in ordered logic – a technique we call substructural operational semantics (SSOS) – manifestly sound program approximations can be derived by simple and intuitive transformations and approximations of the logic program. As examples, we describe how to derive control flow and alias analyses from the substructural operational semantics of the relevant language