Write a Blog >>
Wed 20 Jan 2016 10:30 - 10:55 at Grand Bay North - Track 1: Algorithmic Verification Chair(s): Arie Gurfinkel

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. [17] to fair termination. [17] 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 Jan

POPL-2016-papers
10:30 - 12:10: Research Papers - Track 1: Algorithmic Verification at Grand Bay North
Chair(s): Arie GurfinkelCarnegie Mellon University
POPL-2016-papers10:30 - 10:55
Talk
Akihiro Murase, Tachio TerauchiJAIST, Naoki KobayashiUniversity of Tokyo, Ryosuke SatoUniversity of Tokyo, Hiroshi UnnoUniversity of Tsukuba
POPL-2016-papers10:55 - 11:20
Talk
Gordon Plotkin, Nikolaj BjørnerMicrosoft Research, Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research, George VargheseMicrosoft Research
POPL-2016-papers11:20 - 11:45
Talk
POPL-2016-papers11:45 - 12:10
Talk
Eric KoskinenYale University, Junfeng YangColumbia University