Publication

On Reductions for Synthesis Procedures

Publications associées (35)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Every data structure deserves lock-free memory reclamation

Nachshon Cohen

Memory-management support for lock-free data structures is well known to be a tough problem. Recent work has successfully reduced the overhead of such schemes. However, applying memory-management support to a data structure remains complex and, in many cas ...

2018

Algorithms for the implementation of adaptive isogeometric methods using hierarchical B-splines

Rafael Vazquez Hernandez

In this article we introduce all the ingredients to develop adaptive isogeometric methods based on hierarchical B-splines. In particular, we give precise definitions of local refinement and coarsening that, unlike previously existing methods, can be unders ...

Elsevier2018

Log-Free Concurrent Data Structures

Rachid Guerraoui, Aleksandar Dragojevic, Mihail Igor Zablotchi, Tudor Alexandru David

Non-volatile RAM (NVRAM) makes it possible for data structures to tolerate transient failures, assuming however that programmers have designed these structures such that their consistency is preserved upon recovery. Previous ap- proaches are typically tran ...

USENIX Association2018

Log-Free Concurrent Data Structures

Rachid Guerraoui, Aleksandar Dragojevic, Mihail Igor Zablotchi, Tudor Alexandru David

USENIX ASSOC2018

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

On verifying causal consistency

Rachid Guerraoui, Jad Hamza

Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automaticall ...

Concurrent Search Data Structures Can Be Blocking and Practically Wait-Free

Rachid Guerraoui, Tudor Alexandru David

We argue that there is virtually no practical situation in which one should seek a "theoretically wait-free" algorithm at the expense of a state-of-the-art blocking algorithm in the case of search data structures: blocking algorithms are simple, fast, and ...

ACM2016

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 Verifying Causal Consistency

Rachid Guerraoui, Jad Hamza

2016

Function Passing: A Model for Typed, Distributed Functional Programming

Philipp Haller, Jocelyn Boullier

The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on which to build data-centric distributed systems. A key id ...

Assoc Computing Machinery2016