Publication
Automating Verification of Functional Programs with Quantified Invariants
Related publications (57)
Verification by Reduction to Functional Programs
In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...
EPFL2017Termination of Open Higher-Order Programs
Viktor Kuncak, Nicolas Charles Yves Voirol, Ravichandhran Kandhadai Madhavan
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 am ...
2017Dotty Phantom Types
Martin Odersky, Nicolas Alexander Stucki
Phantom types are a well-known type-level, design pattern which is commonly used to express constraints encoded in types. We observe that in modern, multi-paradigm programming languages, these encodings are too restrictive or do not provide the guarantees ...
2017Configuration logics: Modeling architecture styles
Joseph Sifakis, Simon Bliudze, Anastasia Mavridou, Eduard Baranov
We study a framework for the specification of architecture styles as families of architectures involving a common set of types of components and coordination mechanisms. The framework combines two logics: 1) interaction logics for the specification of arch ...
Elsevier Science Inc2017An Update on Deductive Synthesis and Repair in the Leon Tool
We report our progress in scaling deductive synthesis and repair of recursive functional Scala programs in the Leon tool. We describe new techniques, including a more precise mechanism for encoding the space of meaningful candidate programs. Our techniques ...
2017Solving quantified linear arithmetic by counterexample-guided instantiation
Viktor Kuncak, Andrew Joseph Reynolds
This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...
2017Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization
Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal
We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy eval- uation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. ...
2016On Satisfiability for Quantified Formulas in Instantiation-Based Procedures
Viktor Kuncak, Nicolas Charles Yves Voirol
Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...
2016A semi-continuous formulation for goal-oriented reduced-order models: 1D problems
A semi-continuous formulation is introduced for finding bases that minimise the error in a specific output functional of a reduced-order model. The formulation is advantageous in that it can be used with arbitrary reference data and can be easily applied t ...
Wiley-Blackwell2016On Counter-Example Complete Verification for Higher-Order Functions
Viktor Kuncak, Etienne Kneuss, 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-orde ...
2015