Publication
On Integrating Deductive Synthesis and Verification Systems
Related publications (56)
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 ...
EPFL2017Algorithmic Resource Verification
Ravichandhran Kandhadai Madhavan
Static estimation of resource utilisation of programs is a challenging and important problem with numerous applications. In this thesis, I present new algorithms that enable users to specify and verify their desired bounds on resource usage of functional p ...
EPFL2017Contract-Based Resource Verification for Higher-Order Functions with 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 evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...
Assoc Computing Machinery2017Termination 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 ...
2017An 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 ...
2017Deductive Synthesis and Repair
In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...
EPFL2016A Generic Algorithm for Checking Exhaustivity of Pattern Matching
Algebraic data types and pattern matching are key features of functional programming languages. Exhaustivity checking of pattern matching is a safety belt that defends against unmatched exceptions at runtime and boosts type safety. However, the presence of ...
Assoc Computing Machinery2016A generic algorithm for checking exhaustivity of pattern matching
Algebraic data types and pattern matching are key features of functional programming languages. Exhaustivity checking of pattern matching is a safety belt that defends against unmatched exceptions at runtime and boosts type safety. However, the presence of ...
2016Automating 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 recur ...
2016Verifying 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. ...
2016