Project Details
Projekt
A Scalable Saturation Approach to Higher-Order Verification
Subject Area
Theoretical Computer Science
Term
from 2013 to 2016
Project identifier
Deutsche Forschungsgemeinschaft (DFG) - Project number 232350543
The higher-order functional paradigm, as employed by programming languages including Fsharp, Scala, Haskell and OCaML, is becoming increasingly popular. Applications range from finance through to web services. The growing size and complexity of these applications is leading to larger interest in algorithms and tools to statically analyze and verify higher-order functional code. In the last years the verification community has devoted much effort to studying higher-order model-checking. In particular, a very promising automata-theoretic approach based on collapsible pushdown automata (CPDA) has been developed. This project aims to design scalable model-checking algorithms for verifying safety properties of higher-order functional programs represented as CPDA, and implement them in a prototype tool. The core engine will be based on a saturation algorithm recently discovered in joint work by the first proposer. Saturation algorithms for a class of abstract machines compute the set of predecessors or successors of a given set of configurations of the machine, and so can be used to solve reachability problems.Saturation algorithms for ordinary PDA and generalizations thereofwere introduced in joint work by the second proposer, and have proved highly successful for model checking first-order programs. In particular they have been implemented in the model-checkers MOPED and jMOPED. The project will combine the expertise of the two proposers and the experience gained with MOPED to extend this success to the higher-order case. The project will be carried out in three phases. The first phase will develop a symbolic version of the saturation algorithm of the first proposer, and an algorithm for efficiently computing optimal witnesses. Neither of them can be directly obtained from the existing algorithms for first-order PDA. Optimal witnesses will be used in the second phase to develop a Counter-Example Guided Abstraction Refinement (CEGAR) loop for CPDA. This phase requires to extend predicate abstraction on primitive data types with a new, to be designed notion of secondary abstraction to help mitigate the additional increase in size caused by higher-orders. The third phase will study algorithms to handle pattern matching constructs, which is the main functional staple that cannot be accurately described by the basic CPDA model. We envisage a lazy abstraction technique based on an `approximate' saturation algorithm. Each phase will conclude with an evaluation of the performance of the algorithms on fragments of OCaML and Scala real-world code, and a comparison to other tools.
DFG Programme
Research Grants
