Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

General recursive function

Related publications (22)

Efficient Sequential and Parallel Algorithms for Multistage Stochastic Integer Programming Using Proximity

Friedrich Eisenbrand, Moritz Andreas Venzin, Jana Tabea Cslovjecsek

We consider the problem of solving integer programs of the form min {c^⊺ x : Ax = b, x ∈ ℤ_{⩾ 0}}, where A is a multistage stochastic matrix in the following sense: the primal treedepth of A is bounded by a parameter d, which means that the columns of A ca ...

Schloss Dagstuhl - Leibniz-Zentrum für Informatik2021

Computation Of A 30750-Bit Binary Field Discrete Logarithm

Arjen Lenstra, Thorsten Kleinjung, Robert Granger, Benjamin Pierre Charles Wesolowski

This paper reports on the computation of a discrete logarithm in the finite field F-230750, breaking by a large margin the previous record, which was set in January 2014 by a computation in F-29234. The present computation made essential use of the elimina ...

AMER MATHEMATICAL SOC2021

A finite element framework based on bivariate simplex splines on triangle configurations

Xiaodong Wei

Recently, triangle configuration based bivariate simplex splines (referred to as TCB-spline) have been introduced to the geometric computing community. TCB-splines retain many attractive theoretic properties of classical B-splines, such as partition of uni ...

ELSEVIER SCIENCE SA2019

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

Proactive Synthesis of Recursive Tree-to-String Functions from Examples

Viktor Kuncak, Mikaël Mayer, Jad Hamza

Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute t ...

2017

Verification by Reduction to Functional Programs

Régis William Blanc

In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...

EPFL2017

Deductive Synthesis and Repair

Etienne Kneuss

In this thesis, we explore techniques for the development of recursive functional programs over unbounded domains that are proved correct according to their high-level specifications. We present algorithms for automatically synthesizing executable code, st ...

EPFL2016

On the use of ANOVA expansions in reduced basis methods for high-dimensional parametric partial differential equations

Jan Sickmann Hesthaven

We propose two different improvements of reduced basis (RB) methods to enable the efficient and accurate evaluation of an output functional based on the numerical solution of parametrized partial differential equations with a possibly high-dimensional para ...

Springer Verlag2016

Tensor train approximation of moment equations for elliptic equations with lognormal coefficient

Daniel Kressner, Fabio Nobile, Francesca Bonizzoni

We study an elliptic equation with stochastic coefficient modeled as a lognormal random field. A perturbation approach is adopted, expanding the solution in Taylor series around the nominal value of the coefficient. The resulting recursive deterministic pr ...

Elsevier2016

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...

Springer-Verlag Berlin2015

Developing Verified Software Using Leon

Viktor Kuncak

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

Deductive Program Repair, Computer Aided Verification

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

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

Verifying and Synthesizing Software with Recursive Functions

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

Tight Bounds for Asynchronous Renaming

Rachid Guerraoui, Seth Gilbert, Dan Alistarh

This article presents the first tight bounds on the time complexity of shared-memory renaming, a fundamental problem in distributed computing in which a set of processes need to pick distinct identifiers from a small namespace. We first prove an individual ...

Association for Computing Machinery2014

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

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

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, Philippe Paul Henri Suter, 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

THE NUMBER OF EDGES IN k-QUASI-PLANAR GRAPHS

János Pach

A graph drawn in the plane is called k-quasi-planar if it does not contain k pair-wise crossing edges. It has been conjectured for a long time that for every fixed k, the maximum number of edges of a k-quasi-planar graph with n vertices is O(n). The best k ...

SIAM Publications2013

Integrated Kernel Partitioning and Scheduling for Coarse-Grained Reconfigurable Arrays

Giovanni Ansaloni

Coarse-grained reconfigurable arrays (CGRAs) are a promising class of architectures conjugating flexibility and efficiency. Devising effective methodologies to map applications onto CGRAs is a challenging task, due to their parallel execution paradigm and ...

Institute of Electrical and Electronics Engineers2012

Sub-Logarithmic Test-and-Set Against a Weak Adversary

Dan Alistarh

A randomized implementation is given of a test-and-set register with O(log log it) individual step complexity and O(n) total step complexity against an oblivious adversary. The implementation is linearizable and multi-shot, and shows an exponential complex ...

Springer-Verlag Berlin2011