Publication

Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)

Related publications (36)

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.

High-level synthesis of dataflow programs for heterogeneous platforms

Endri Bezati

The growing complexity of digital signal processing applications implemented in programmable logic and embedded processors make a compelling case the use of high-level methodologies for their design and implementation. Past research has shown that for comp ...

EPFL2015

Synthesis and optimization of high-level stream programs

Marco Mattavelli, Simone Casale Brunet, Endri Bezati

In this paper we address the problem of translating high-level stream programs, such as those written in MPEG's RVC-CAL dataflow language, into implementations in programmable hardware. Our focus is on two aspects: sufficient language coverage to make synt ...

2013

Synthesis And Optimization Of High-Level Stream Programs

Marco Mattavelli, Simone Casale Brunet, Endri Bezati

Ieee2013

High-Level Synthesis of Dataflow Programs for Signal Processing Systems

Marco Mattavelli, Endri Bezati

The growing complexity of signal processing algorithms and platforms poses significant challenges to design methods and implementation tools. High-level dataflow programs, such as those in MPEG's RVC-CAL language, provide abstraction and the opportunity fo ...

2013

Protecting Privacy through Distributed Computation in Multi-agent Decision Making

Boi Faltings, Thomas Léauté

As large-scale theft of data from corporate servers is becoming increasingly common, it becomes interesting to examine alternatives to the paradigm of centralizing sensitive data into large databases. Instead, one could use cryptography and distributed com ...

AI Access Foundation2013

Constraints as Control

Viktor Kuncak, Philippe Paul Henri Suter

We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates con ...

2012

Constraints as Control

Viktor Kuncak, Philippe Paul Henri Suter

ACM Order Department, P O Box 64145, Baltimore, MD 21264 Usa2012

Stochastic Model Predictive Control: Controlling the Average Number of Constraint Violations

Colin Neil Jones, Milan Korda

This paper considers linear discrete-time systems with additive bounded disturbances subject to hard control input bounds and constraints on the expected number of state-constraint violations averaged over time, or, equivalently, constraints on the probabi ...

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 Deciding Functional Lists with Sublist Sets

Viktor Kuncak

Motivated by the problem of deciding verification conditions for the verification of functional programs, we present new decision procedures for automated reasoning about functional lists. We first show how to decide in NP the satisfiability problem for lo ...

2010