Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Computer Aided Verification
Graph Chatbot
Chat with Graph Search
Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.
DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
