Concept

General recursive function

Related publications (42)

Developing Verified Software Using Leon

We present Leon, a system for developing functional Scala programs annotated with contracts. Contracts in Leon can themselves refer to recursively defined functions. Leon aims to find counterexamples when functions do not meet the specifications, and proof ...

Springer-Verlag Berlin2015

On Deductive Program Repair in Leon

Viktor Kuncak, Etienne Kneuss

We present an approach to program repair and its application to programs with recursive functions over unbounded data types. Our approach formulates program repair in the framework of deductive synthesis that uses existing program structure as a hint to gu ...

2015

Deductive Program Repair, Computer Aided Verification

Viktor Kuncak, Etienne Kneuss

2015

Explicit Recursive and Adaptive Filtering in Reproducing Kernel Hilbert Spaces

Devis Tuia

This brief presents a methodology to develop recursive filters in reproducing kernel Hilbert spaces. Unlike previous approaches that exploit the kernel trick on filtered and then mapped samples, we explicitly define the model recursivity in the Hilbert spa ...

Ieee-Inst Electrical Electronics Engineers Inc2014

Symbolic Resource Bound Inference

Viktor Kuncak, Ravichandhran Kandhadai Madhavan

We present an approach for inferring symbolic resource bounds for purely functional programs consisting of recursive functions, algebraic data types and nonlinear arithmetic operations. In our approach, the developer specifies the desired shape of the boun ...

2014

Verifying and Synthesizing Software with Recursive Functions (Invited Contribution)

Viktor Kuncak

Our goal is to help people construct software that does what they wish. We develop tools and algorithms that span static and dynamic verification, constraint solving, and program synthesis. I will outline the current state our verification and synthesis sy ...

Springer-Verlag Berlin2014

MATHICSE Technical Report : Tensor train approximation of moment equations for the log-normal Darcy problem

Fabio Nobile, Daniel Kressner, Francesca Bonizzoni

We study the Darcy problem with log-normal permeability, modeling the fluid flow in a heterogeneous porous medium. A perturbation approach is adopted, expanding the solution in Taylor series around the nominal value of the permeability. The resulting recur ...

MATHICSE2014

Interactive Function Computation

Michael Christoph Gastpar

We investigate the role of interaction for computa- tion problem settings where nodes intend to compute functions of the raw messages generated at other nodes. In this work, we make some progress on a more elementary research component: feedback. Specifica ...

2013

An overview of the Leon verification system: verification by translation to recursive functions

Viktor Kuncak, Etienne Kneuss, Régis William Blanc, Philippe Paul Henri Suter

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

Synthesis Modulo Recursive Functions

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

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

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.