Publication
Refutation-based synthesis in SMT
Related publications (32)
Scaling Language Features for Program Verification
Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
EPFL2022Scaling Functional Synthesis and Repair
Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...
EPFL2019Verified Functional Programming
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 solve ...
EPFL2019A new analysis approach for T-2 relaxometry myelin water quantification: Orthogonal Matching Pursuit
Purpose: In vivo myelin quantification can provide valuable noninvasive information on neuronal maturation and development, as well as insights into neurological disorders. Multiexponential analysis of multiecho T-2 relaxation is a powerful and widely appl ...
WILEY2019LMS-Verify: Abstraction without Regret for Verified Systems Programming’
Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...
Assoc Computing Machinery2017Algorithmic 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 ...
EPFL2017An 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 ...
2017Exploiting Satisfiability Solvers for Efficient Logic Synthesis
Logic synthesis is an important part of electronic design automation (EDA) flows, which enable the implementation of digital systems. As the design size and complexity increase, the data structures and algorithms for logic synthesis must adapt and improve ...
EPFL2017Automating 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 ...
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 ...
2016