Publication

Decision Procedures for Program Synthesis and Verification

Publications associées (95)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Sound Compilation of Reals

Viktor Kuncak, Eva Darulova

Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming model where the user writes a program in a real-valued implementation and sp ...

ACM2014

On Induction for SMT Solvers

Viktor Kuncak, Andrew Joseph Reynolds

Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas ...

2014

Lightweight Snapshots and System-level Backtracking

George Candea, Edouard Bugnion, Vitaly Chipounov

We propose a new system-level abstraction, the lightweight immutable execution snapshot, which combines the immutable characteristics of checkpoints with the direct integration into the virtual memory subsystem of standard mutable address spaces. The abstr ...

USENIX2013

Tree Interpolation in Vampire

Régis William Blanc, Laura Ildiko Kovacs, Ashutosh Gupta

We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of ...

Springer Berlin Heidelberg2013

Interpolation for Synthesis on Unbounded Domains

Viktor Kuncak, Régis William Blanc

Synthesis procedures compile relational specifications into functions. In addition to bounded domains, synthesis procedures are applicable to domains such as mathematical integers, where the domain and range of relations and synthesized code is unbounded. ...

Ieee2013

Techniques for Program Synthesis

Régis William Blanc

Software synthesis is an attractive field of study that can promise a more safe and productive software development process. However, it is notoriously very difficult and few convincing applications have emerged so far. In this report, we present a series ...

2013

Software Synthesis Procedures

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succ ...

2012

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

STM in the Small: Trading Generality for Performance in Software Transactional Memory

Aleksandar Dragojevic

Data structures implemented using software transactional memory (STM) have a reputation for being much slower than data structures implemented directly from low-level primitives such as atomic compare-and-swap (CAS). In this paper we present a specialized ...

2012

On Reductions for Synthesis Procedures

Viktor Kuncak, Philippe Paul Henri Suter, Swen Jacobs

A synthesis procedure acts as a compiler for declarative specifications. It accepts a formula describing a relation between inputs and outputs, and generates a function implementing this relation. This paper presents synthesis procedures for data structure ...

2012