Temporal Verification of Higher-order Functional Programs
We present an automated approach to verifying arbitrary omega-regular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties.
Our approach is automata-theoretic, and extends the recently proposed binary-reachability-based approach to automated termination verification of higher-order functional programs by Kuwahara et al.  to fair termination.  has shown that checking disjunctive well-foundedness of (the transitive closure of) ``calling relation'' is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.
Wed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10
Track 1: Algorithmic VerificationResearch Papers at Grand Bay North
Chair(s): Arie Gurfinkel Carnegie Mellon University
|Temporal Verification of Higher-order Functional Programs|
Akihiro Murase , Tachio Terauchi JAIST, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo, Hiroshi Unno University of Tsukuba
|Scaling Network Verification using Symmetry and Surgery|
Gordon Plotkin , Nikolaj Bjørner Microsoft Research, Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research, George Varghese Microsoft ResearchPre-print
|Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates|
|Reducing Crash Recoverability to Reachability|
Eric Koskinen Yale University, Junfeng Yang Columbia University