[hofa] Logical approximation for program analysis
David Van Horn
dvanhorn at ccs.neu.edu
Wed Jun 22 13:28:03 PDT 2011
This is really interesting work that I wanted to share with the HOFA
list. It first appeared at PEPM'09 and has now been published by HOSC.
David
Logical approximation for program analysis
Higher-Order and Symbolic Computation
Robert J. Simmons and Frank Pfenning
http://www.springerlink.com/content/1h33370m88857897/
The abstract interpretation of programs relates the exact semantics of a
programming language to a finite approximation of those semantics. In
this article, we describe an approach to abstract interpretation that is
based in logic and logic programming.
Our approach consists of faithfully representing a transition system
within logic and then manipulating this initial specification to create
a logical approximation of the original specification. The objective is
to derive a logical approximation that can be interpreted as a
terminating forward-chaining logic program; this ensures that the
approximation is finite and that, furthermore, an appropriate logic
programming interpreter can implement the derived approximation.
We are particularly interested in the specification of the operational
semantics of programming languages in ordered logic, a technique we call
substructural operational semantics (SSOS). We show that manifestly
sound control flow and alias analyses can be derived as logical
approximations of the substructural operational semantics of relevant
languages.
More information about the HOFA
mailing list