Logic-flow analysis of higher-order programs

10 years 12 months ago
Logic-flow analysis of higher-order programs
This work presents a framework for fusing flow analysis and theorem proving called logic-flow analysis (LFA). The framework itthe reduced product of two abstract interpretations: (1) an state machine and (2) a set of propositions in a restricted first-order logic. The motivating application for LFA is the safe removal of implicit array-bounds checks without type information, user interaction or program annotation. LFA achieves this by delegating a given task to either the prover or the flow analysis depending on which is best suited to discharge it. Described within are a concrete semantics for continuation-passing style; a restricted, firstgic; a woven product of two abstract interpretations; proofs of correctness; and a worked example. Categories and Subject Descriptors D.3.4 [Programming Languages]: Processors--Optimization General Terms Languages Keywords logic-flow analysis, LFA, static analysis, environment analysis, lambda calculus, CPS, abstract garbage collection, abstract co...
Matthew Might
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Matthew Might
Comments (0)