Termination of Open Higher-Order Programs

We study the problem of proving termination of open, higher-order programs with recursive functions and datatypes. We identify a new point in the design space of solutions, with an appealing trade-off between simplicity of specification, modularity, and amenability to automation. Specifically, we consider termination of open expressions in the presence of higher-order, recursive functions, and introduce a new notion of termination that is conditioned on the termination of the callbacks made by the expressions. For closed expressions our definition coincides with the traditional definition of termination. We derive sound proof obligations for establishing termination modulo callbacks, and develop a modular approach for verifying the obligations. Our approach is novel in three aspects. (a) It allows users to express properties about the environment in the form of higher-order contracts. (b) It establishes properties on the creation sites of closures instead of application sites and does not require knowing the targets of applications. (c) It uses a modular reasoning where termination (modulo callbacks) is verified for each function independently and then composed to check termination of their callers. We present the results of evaluating our approach on benchmarks comprising more than 10K lines of functional Scala code. The results show that our approach, when combined with a safety verifier, established both termination and safety of complex algorithms and data structures that are beyond the reach of state-of-the-art techniques. For example, it verifies Okasaki's scheduling-based data structures and lazy trees in under a few seconds.

Automating Verification of Functional Programs with Quantified Invariants

Viktor Kuncak, Nicolas Charles Yves Voirol

We present the foundations of a verifier for higher-order functional programs with generics and recursive algebraic data types. Our ver- ifier supports finding sound proofs and counterexamples even in the presence of certain quantified invariants and recursive functions. Our approach uses the same language to describe programs and in- variants and uses semantic criteria for establishing termination. Our implementation makes effective use of SMT solvers by encoding first-class functions and quantifiers into a quantifier-free fragment of first-order logic with theories. We are able to specify properties of datastructure operations involving higher-order functions with minimal annotation overhead and verify them with a high degree of automation. Our system is also effective at reporting counterexam- ples, even in the presence of first-order quantification.

2016

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solvers to automate the verification process and to provide us with useful counterexamples when considered properties are invalid. We then enable verification in the presence of high-level Scala language features by encoding them into the dependently-typed language. We introduce an SMT-backed counterexample finding procedure which can also prove that no counterexample exists. The procedure incrementally unfolds function calls and applications in order to progressively explore the space of counterexamples. We present increasingly expressive fragments of our dependently-typed language and establish soundness and completeness properties of the procedure for each fragment. We then describe an extension which introduces support for quantifier reasoning. We discuss syntactic and semantic conditions under which the extended procedure can produce valid counterexamples in the presence of universal quantification. We present a bidirectional type checking algorithm for our dependent type system. The algorithm relies on our counterexample finding procedure to discharge verification conditions which enables predictable and effective type checking. The type system features a unified treatment of both recursive and corecursive definitions, and further admits mutual recursion between type and function definitions. We establish normalization through a sized types approach. We define a logical relation which associates a set of reducible values to each type, and then show soundness of verification by proving that evaluation of a type checked expression terminates with a reducible value. We further discuss a set of transformations which encode high-level Scala constructs into our dependently-typed language. These transformations allow our verification system to support object-oriented features such as traits and classes with multiple inheritance, as well as abstract and concrete methods with overriding. We further present a measure inference transformation which enables automated termination checking in our system. In addition to encoding language features, we discuss how Scala can be augmented with natural specification constructs and annotations that empower verification. Finally, we describe the system implementation and discuss certain practical considerations. We show that the resulting system is effective by evaluating it on a set of benchmarks and case studies comprising over 15K lines of Scala code. These benchmarks showcase both the breadth and flexibility of the system.

EPFL2019

On Counter-Example Complete Verification for Higher-Order Functions

Etienne Kneuss, Viktor Kuncak, Nicolas Charles Yves Voirol

We present a verification procedure for pure higher-order functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counter-examples. The procedure reduces the analysis of higher-order programs to checking satisfiability of a sequence of quantifier-free formulas over theories such as algebraic data types, integer linear arithmetic, and uninterpreted function symbols, thus enabling the use of efficient satisfiability modulo theory (SMT) solvers. Our solution supports arbitrary function types and arbitrarily nested anonymous functions (which can be stored in data structures, passed as arguments, returned, and applied). Among the contributions of this work is supporting even those cases when anonymous functions cannot be statically traced back to their definition, ensuring completeness of the approach for finding counter-examples. We provide a proof of soundness and counter-example completeness for our system as well as initial evaluation in the Leon verifier.

2015

Verified Functional Programming

Nicolas Charles Yves Voirol

EPFL2019