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

• Type: Conference
• Year: 2007
• Where: POPL
• Authors: Matthew Might
• Keywords: First-order Logic, Implicit Array-bounds Checks, POPL 2007, Processors--Optimization General Terms, Programming Languages