Carnegie Mellon University
file.pdf (322.66 kB)
Download file

Logical approximation for program analysis

Download (322.66 kB)
journal contribution
posted on 2009-09-01, 00:00 authored by Robert J. Simmons, Frank Pfenning
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 languages




Usage metrics