Publication

Refutation-based synthesis in SMT

Related publications (20)

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 ...

EPFL2022

Revisiting Explicit Enumeration for Exact Synthesis

Heinz Riener

The problem of generating a minimal implementation of a given Boolean function is called exact synthesis. The parameter to be minimized is often the total number of gates used for the implementation. The exact synthesis engine is considered an essential to ...

IEEE COMPUTER SOC2020

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

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 ...

EPFL2019

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 solve ...

EPFL2019

A new analysis approach for T-2 relaxometry myelin water quantification: Orthogonal Matching Pursuit

Guillaume Jean Op 't Veld

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 ...

Wiley2019

LMS-Verify: Abstraction without Regret for Verified Systems Programming’

Nada Amin, Tiark Rompf

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 Machinery2017

Algorithmic 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 ...

EPFL2017

An Update on Deductive Synthesis and Repair in the Leon Tool

Etienne Kneuss, Viktor Kuncak, Emmanouil Koukoutos

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 ...

2017

Exploiting Satisfiability Solvers for Efficient Logic Synthesis

Ana Petkovska

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 ...

EPFL2017

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Computer Aided Verification

Viktor Kuncak, Andrew Joseph Reynolds

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 ...

2015

Synthesis Modulo Recursive Functions

Philippe Paul Henri Suter, Etienne Kneuss, Viktor Kuncak, Ivan Kuraj

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synt ...

2013

Alpha-synuclein Post-translational Modifications as Potential Biomarkers for Parkinson Disease and Other Synucleinopathies

Bruno Claude Daniel Fauvet, Hilal Lashuel, Adrian Schmid, Marc Moniatte

The development of novel therapies against neurodegenerative disorders requires the ability to detect their early, presymptomatic manifestations in order to enable treatment before irreversible cellular damage occurs. Precocious signs indicative of neurode ...

Amer Soc Biochemistry Molecular Biology Inc2013

Programming with Specifications

Philippe Paul Henri Suter

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...

EPFL2012

Towards Complete Reasoning about Axiomatic Specifications

Viktor Kuncak, Swen Jacobs

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Building a Calculus of Data Structures

Philippe Paul Henri Suter, Viktor Kuncak, Ruzica Piskac

Techniques such as verification condition generation, predicate abstraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Programs and their specifications often make use of data structures such as sets ...

Springer2010

Software Verification by Combining Program Analyses of Adjustable Precision

Grégory Théoduloz

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...

EPFL2010

Shape Refinement through Explicit Heap Analysis

Grégory Théoduloz, Dirk Thilo Beyer, Damien Zufferey

Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structu ...

Springer2010

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

Laura Ildiko Kovacs

We present a new method for automatic generation of loop invariants for programs containing arrays. Unlike all previously known methods, our method allows one to generate first-order invariants containing alternations of quantifiers. The method is based on ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2009

Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...

Springer2009

Decision Procedures for Multisets with Cardinality Constraints

Viktor Kuncak, Ruzica Piskac

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...

Springer2008