Publications associées à Finding Almost-Invariants in Distributed Systems

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain ...

Assoc Computing Machinery2024

Automated Formal Verification of Software Network Functions

Solal Vincenzo Pirelli

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Reliable Microsecond-Scale Distributed Computing

Athanasios Xygkis

The landscape of computing is changing, thanks to the advent of modern networking equipment that allows machines to exchange information in as little as one microsecond. Such advancement has enabled microsecond-scale distributed computing, where entire dis ...

EPFL2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

The SparSpec algorithm and the application to the detection of spatial periodicities in tokamaks: from a 1D to a 2D analysis

Duccio Testa

A well-known, previously only 1D, algorithm using the Sparse Representation of Signals and an iterative Block Coordinate Descent method (the SparSpec-1D algorithm) has been further developed and tested in a 2D spatial domain to obtain the toroidal and polo ...

2022

Dynamic Byzantine Reliable Broadcast

Rachid Guerraoui, Dragos-Adrian Seredinschi, Jovan Komatovic, Andrei Tonkikh

Reliable broadcast is a communication primitive guaranteeing, intuitively, that all processes in a distributed system deliver the same set of messages. The reason why this primitive is appealing is twofold: (i) we can implement it deterministically in a co ...

Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik2021

Preventing Use-After-Free Attacks with Fast Forward Allocation

Jungwon Lim, Sanidhya Kashyap

Memory-unsafe languages are widely used to implement critical systems like kernels and browsers, leading to thousands of memory safety issues every year. A use-after-free bug is a temporal memory error where the program accidentally visits a freed memory l ...

USENIX ASSOC2021

Asynchronous distributed coordination and consensus with threshold logical clocks

Bryan Alexander Ford

Consensus protocols for asynchronous networks are usually complex and inefficient, leading practical systems to rely on synchronous protocols. The invention proposes an approach to simplify asynchronous consensus by building it atop a novel threshold logic ...

2021

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

System Support for Efficient Replication in Distributed Systems

Dragos-Adrian Seredinschi

Current online applications, such as search engines, social networks, or file sharing services, execute across a distributed network of machines. They provide non-stop services to their users despite failures in the underlying network. To achieve such a hi ...

EPFL2019

Managing Tail Latency in Datacenter-Scale File Systems Under Production Constraints

Willy Zwaenepoel, Ricardo Bianchini, Maria Fernanda Borge Chavez

Distributed file systems often exhibit high tail latencies, especially in large-scale datacenters and in the presence of competing (and possibly higher priority) workloads. This paper introduces techniques for managing tail latencies in these systems, whil ...

ASSOC COMPUTING MACHINERY2019

Experimenting with knots

Giovanni Dietler

Knots are interesting objects to experiment since their topological properties are combined with mechanical properties, fluid mechanics or dynamical properties like unknotting under the excitation of the thermal energy. Knots play also a role in biology be ...

SPRINGER HEIDELBERG2019

Integration of ecosystem services in regional spatial plans in Western Switzerland

Jérôme Chenal, Rémi Jaligot

The concept of ecosystem services (ES) is regarded as an increasingly important framework and tool to support spatial planning. A limited understanding of how ES knowledge is used in spatial plans constrains our ability to learn from, replicate, and convey ...

2019

Theory and Practice of Coroutines with Snapshots

Aleksandar Prokopec, Fengyun Liu

While event-driven programming is a widespread model for asynchronous computing, its inherent control flow fragmentation makes event-driven programs notoriously difficult to understand and maintain. Coroutines are a general control flow construct that can ...

2018

Distributed Transactions: Dissecting the Nightmare

Rachid Guerraoui, Willy Zwaenepoel, Junxiong Wang, Diego Didona

Many distributed storage systems are transactional and a lot of work has been devoted to optimizing their performance, especially the performance of read-only transactions that are considered the most frequent in practice. Yet, the results obtained so far ...

2018

The Disclosure Power of Shared Objects

Rachid Guerraoui, Mihail Igor Zablotchi, Peva François Blanchard, Julien Michel Stainer

Shared objects are the means by which processes gather and exchange information about the state of a distributed system. Objects that disclose more information about the system are therefore more desirable. In this paper, we propose the schedule reconstruc ...

2017

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 ...

Optimal Sensor Architecture Selection for Health Management of Complex Systems

Martin Vetterli, Juri Ranieri

With technological progress, humans tend to create engineering systems with constantly increasing complexity and higher operational requirements. Many complex systems require the use of a Health Management (HM) solution to ensure safety and enable lifecycl ...

Ieee2016

Synthesizing efficient systems in probabilistic environments

Barbara Jobstmann, David Parker

We present a formalism, algorithms and tools to synthesise reactive systems that behave efficiently, i.e., which achieve an optimal trade-off between a given cost and reward model. Synthesis aims to automatically generate a program from a specification. Mo ...

Springer2016

Automatic generation of program execution that reaches a given failure point

George Candea, Cristian Zamfir

An execution of a target software program that causes a particular bug to manifest itself is generated. A target software program is received. A bug report generated by an execution of the target software program is received. The bug report describes a par ...

2015