[hofa] Logical approximation for program analysis

[David Van Horn]

I just came across this:

Logical approximation for program analysis
Robert J. Simmons, Frank Pfenning
HOSC

http://www.cs.cmu.edu/~rjsimmon/papers/simmons11logical.pdf

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.