Template polyhedra with a twist

Abstract

In this paper, we draw upon connections between bilinear programming and the process of computing (post) fixed points in abstract interpretation. It is well-known that the data flow constraints for numerical domains are expressed in terms of bilinear constraints. Algorithms such as policy and strategy iteration have been proposed for the special case of bilinear constraints that arise from template numerical domains. In particular, policy iteration improves upon a known post-fixed point by alternating between solving for an improved post-fixed point against finding certificates that are used to prove the new fixed point. In this paper, we draw upon these connections to formulate a policy iteration scheme that changes the template on the fly in order to prove a target reachability property of interest. We show how the change to the template naturally fits inside a policy iteration scheme, and thus propose a policy iteration scheme that updates the template matrices associated with each program location. We demonstrate that the approach is effective over a set of benchmark instances, wherein starting from a simple predefined choice of templates, the approach is able to infer appropriate template directions to prove a property of interest. We also note some key theoretical questions regarding the convergence of the policy iteration scheme with template updates, that remain open at this time.