We’ve been working on two techniques for systematically deriving abstract interpretations approximating canonical machines for higher-order languages. The first allocates continuations in a bounded store to achieve a finite state-space. We demonstrate the generality of this approach by transforming classical abstract machines into abstract interpreters.
Abstracting Abstract Machines.
David Van Horn and Matthew Might.
The 15th ACM SIGPLAN [...]
A new preprint by Matthew Might, Yannis Smaragdakis, and David Van Horn.
Preprint
Slides from NEPLS
Implementation
Abstract:
Low-level program analysis is a fundamental problem, taking the shape of “flow analysis” in functional languages and “points-to” analysis in imperative and object-oriented (OO) languages. Despite the similarities, the vocabulary and results in the two communities remain largely distinct, with limited [...]
The Higher-Order Flow Analysis Forum has just been set up:
The HOFA forum is an email forum for the discussion and dissemination of research results in the area of higher-order flow analysis, broadly construed, within computer science and related disciplines. Flow analysis and related static analyses are a fundamental tool for program verification, bug detection, compiler [...]
The Complexity of Flow Analysis in Higher-Order Languages: Abstract, Dissertation, Slides.
PhD Thesis Defense
Computer Science Department
Brandeis University
Date: Wednesday, July 22, 2009
Time: 2-4pm
Place: Volen 101
The Complexity of Flow Analysis in Higher-Order Languages
David Van Horn
Abstract:
This dissertation proves lower bounds on the inherent difficulty of deciding flow analysis problems in higher-order programming languages. We give exact characterizations of the computational complexity of 0CFA, the kCFA hierarchy, and related analyses. [...]
Subcubic Control Flow Analysis Algorithms, Jan Midtgaard and David Van Horn.
We give the first direct subcubic algorithm for performing control flow analysis of higher-order functional programs. Despite the long held belief that inclusion-based flow analysis could not surpass the “cubic bottleneck, ” we apply known set compression techniques to obtain an algorithm that runs in [...]
Accepted papers for the 2009 ICFP have been announced and several look quite interesting. Midtgaard and Jensen’s “Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation” is available as a TR here. PLT has an impressive showing, and Ralf Hinze’s “La Tour D’Hanoï” is sure to be fun.
Flow analysis, linearity, and PTIME was accepted at this year’s Static Analysis Symposium (SAS). An early preprint was announced here, but the presentation has benefitted significantly from the anonymous reviewers’ comments. Also, the abstract was rewritten to be somewhat comprehensible (thanks to Dave Herman for encouraging the rewrite).
Flow analysis is a ubiquitous [...]
A new preprint is available (submitted to ICFP), Deciding kCFA is complete for EXPTIME:
We give an exact characterization of the computational complexity of the kCFA hierarchy. For any k > 0, we prove that the control flow decision problem is complete for deterministic exponential time. This theorem validates empirical observations that such control [...]
Jan Midtgaard’s survey, Control-Flow Analysis of Functional Programs, has just been published as a BRICS technical report. This is a paper I wish I could have read when I started my research on flow analysis. As it was, I read it only after I was already deep in the thicket, and yet I [...]