Publication

Functional synthesis for linear arithmetic and sets

Related publications (52)

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.

On Software Verification and Graph Similarity for Automated Evaluation of Students' Assignments

Viktor Kuncak

The number of students enrolled in universities at standard and online programming courses is huge. This calls for automated evaluation of students assignments and for automated support for learning. We aim at developing methods and tools for objective and ...

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

Comfusy: A Tool for Complete Functional Synthesis

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

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. We present Comfusy, a tool that extends the compiler for the general-purpose programming language Scala with (non-reactive) functional synthesi ...

Springer2010

On Complete Functional Synthesis

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

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way---they should succeed for a well-def ...

2009

On Set-Driven Combination of Logics and Verifiers

Viktor Kuncak

We explore the problem of automated reasoning about the non-disjoint combination of logics that share set variables and operations. We prove a general combination theorem, and apply it to show the decidability for the quantifier-free combination of formula ...

2009

Computer Code as a Medium for Human Communication: Are Programming Languages Improving?

Gilles Dubochet

Programming languages are not only useful to command computers, they also increasingly are a medium for human communication. I will use the framework of distributed cognition to discuss how knowledge is shared in a team of programmers and to show that comp ...

University of Limerick2009

Overview of the MPEG Reconfigurable Video Coding Framework

Marco Mattavelli, Christophe Lucarz

Video coding technology in the last 20 years has evolved producing a variety of diff erent and complex algorithms and coding standards. So far the speciﬁcation of such standards, and of the algorithms that build them, has been done case by case providing m ...

2009

Singularity: Rethinking the Software Stack

James Richard Larus

Every operating system embodies a collection of design decisions. Many of the decisions behind today's most popular operating systems have remained unchanged, even as hardware and software have evolved. Operating systems form the foundation of almost every ...

ACM2007

Distributed Consensus, Revisited

Rachele Fuzzati, Massimo Merro

We provide a novel model to formalize a well-known algorithm, by Chandra and Toueg, that solves Consensus among asynchronous distributed processes in the presence of a particular class of failure detectors (Diamond S or, equivalently, Omega), under the hyp ...

2007

Efficient Semi-structured Queries in Scala using XQuery Shipping

This project proposes a new approach to interact with database systems through programming languages. A formal query language can be integrated within modern programming languages and the semi-structured queries can be evaluated using automatic transformat ...

2006