[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.


Logical approximation for program analysis
Higher-Order and Symbolic Computation
Robert J. Simmons and Frank Pfenning

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 

More information about the HOFA mailing list