Exact flow analysis by higher-order model checking. (English) Zbl 1354.68050

Tobita, Yoshihiro; Tsukada, Takeshi; Kobayashi, Naoki

Schrijvers, Tom (ed.) et al., Functional and logic programming. 11th international symposium, FLOPS 2012, Kobe, Japan, May 23–25, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-29821-9/pbk). Lecture Notes in Computer Science 7294, 275-289 (2012).

Summary: 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 \(\lambda\)-calculus with recursion and finite base types, and that, unlike C. Mossin’s exact flow analysis [Math. Struct. Comput. Sci. 13, No. 1, 125–156 (2003; Zbl 1031.68045)], 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.
For the entire collection see [Zbl 1241.68038].

MSC:

68N18	Functional programming and lambda calculus
68Q60	Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 1031.68045

Software:

TRecS; THORS; EigenCFA