We propose a novel control flow analysis for higher-order functional programs, based on a reduction to higher-order model checking. The distinguished features of our control flow analysis are that, unlike most of the control flow analyses like k-CFA, it is exact for simply-typed (λ)-calculus with recursion and finite base types, and that, unlike Mossin's exact flow analysis, it is indeed runnable in practice, at least for small programs. Furthermore, under certain (arguably strong) assumptions, our control flow analysis runs in time cubic in the size of a program. We formalize the reduction of control flow analysis to higher-order model checking, prove the correctness, and report preliminary experiments. © 2012 Springer-Verlag.
CITATION STYLE
Tobita, Y., Tsukada, T., & Kobayashi, N. (2012). Exact flow analysis by higher-order model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7294 LNCS, pp. 275–289). https://doi.org/10.1007/978-3-642-29822-6_22
Mendeley helps you to discover research relevant for your work.