Publication

Symbolic Resource Bound Inference

Related publications (68)

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.

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

On Integrating Deductive Synthesis and Verification Systems

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

2013

A Speculation-Friendly Binary Search Tree

Vincent Gramoli

We introduce the first binary search tree algorithm designed for speculative executions. Prior to this work, tree structures were mainly designed for their pessimistic (non-speculative) accesses to have a bounded complexity. Researchers tried to evaluate t ...

Assoc Computing Machinery2012

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

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

Corporate structure optimisation for multinational companies

In this paper we consider a multinational corporate structuring problem. This problem involves designing a corporate/organisational structure (across different countries) so as to remit profits from a number of subsidiaries to a single parent company, whil ...

2012

Models capturing latent constructs

Michel Bierlaire, Aurélie Glerum

In the context of the development of hybrid choice models (HCM), we are interested in understanding better how to design models which can account for the latent information contained in new data types (psychometrics, data from smartphones, etc.) for which ...

2011

Towards Complete Reasoning about Axiomatic Specifications

Viktor Kuncak, Swen Jacobs

To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011

Automated Reconstruction of Dendritic and Axonal Trees by Global Optimization with Geometric Priors

Pascal Fua, Engin Türetken, Germán González Serrano

We present a novel probabilistic approach to fully automated delineation of tree structures in noisy 2D images and 3D image stacks. Unlike earlier methods that rely mostly on local evidence, ours builds a set of candidate trees over many different subsets ...

Humana Press2011

PLP: Page Latch-free Shared-everything OLTP

Anastasia Ailamaki, Frederick Ryan Johnson, Pinar Tözün, Ippokratis Pandis

Scaling the performance of shared-everything on-line transaction processing to highly-parallel multicore hardware remains a great challenge for database system designers. Developments in OLTP technology remove locking and logging from being scalability bot ...

2011