Publications associées à Distributed Consensus, Revisited

Automated Formal Verification of Software Network Functions

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

Formal Foundations of Capture Tracking

Aleksander Slawomir Boruch-Gruszecki

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...

EPFL2024

Planetary-Scale Byzantine Fault Tolerance

Matteo Monti

The scale and pervasiveness of the Internet make it a pillar of planetary communication, industry and economy, as well as a fundamental medium for public discourse and democratic engagement. In stark contrast with the Internet's decentralized infrastructur ...

EPFL2024

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Yichen Xu

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

Analytical Computation of the Sensitivity Coefficients in Hybrid AC/DC Networks

Mario Paolone, Willem Lambrichts

In this paper, we present a model for the analytical computation of the power flow sensitivity coefficients (SCs) for hybrid AC/DC networks. The SCs are defined as the partial derivates of the nodal voltages with respect to the active and reactive power in ...

2024

Reach For the Arcs: Reconstructing Surfaces from SDFs via Tangent Points

Yingying Ren

We introduce an algorithm to reconstruct a mesh from discrete samples of a shape's Signed Distance Function (SDF). A simple geometric reinterpretation of the SDF lets us formulate the problem through a point cloud, from which a surface can be extracted wit ...

Association for Computing Machinery2024

A ride time-oriented scheduling algorithm for dial-a-ride problems

Nikolaos Geroliminis, Claudia Bongiovanni, Mor Kaspi

This paper offers a new algorithm to efficiently optimize scheduling decisions for dial-a-ride problems (DARPs), including problem variants considering electric and autonomous vehicles (e-ADARPs). The scheduling heuristic, based on linear programming theor ...

Pergamon-Elsevier Science Ltd2024

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

On Speed and Advantage : Results in Information Velocity and Monitoring Problems

Reka Inovan

Information theory has allowed us to determine the fundamental limit of various communication and algorithmic problems, e.g., the channel coding problem, the compression problem, and the hypothesis testing problem. In this work, we revisit the assumptions ...

EPFL2024

Dynamic Linkers Are the Narrow Waist of Operating Systems

Adrien Ghosn, Charly Nicolas Lucien Castes

While software applications, programming languages, and hardware have changed, operating systems have not. Widely-used commodity operating systems are still modeled after the ones designed in the seventies. The accumulated burden of backward compatibility ...

Association for Computing Machinery2023

SiliFish: A desktop application to model swimming behavior in developing zebrafish (Danio rerio)

Yann Roussel

SiliFish is an open-source desktop application tomodel and study zebrafish swimming. Here, we explain how to define the general parameters of the model, define cell populations, place them within the spinal cord, and define their projections. We explain ho ...

Elsevier2023

Not Yet Another Digital ID: Privacy-Preserving Humanitarian Aid Distribution

Justinas Sukaitis, Carmela González Troncoso, Wouter Lueks, Boya Wang

Humanitarian aid-distribution programs help bring physical goods to people in need. Traditional paper-based solutions to support aid distribution do not scale to large populations and are hard to secure. Existing digital solutions solve these issues, at th ...

IEEE COMPUTER SOC2023

Ferroelectric device or structure and a method for producing ferroelectric devices or structures

Rui Ning Wang, Tobias Kippenberg, Zelin Tan

The present invention concerns a method for producing at least one ferroelectric device or structure comprising the steps of providing at least one ferroelectric material or layer, or providing at least one ferroelectric material or layer to be patterned o ...

2023

High-precision optical magnetometry using Nitrogen Vacancies in CVD diamond

Hossein Babashah

Sensing weak magnetic fields is a topic of great importance in basic science and technology due to its wide range of applications. In this context, solid-state and nanoscale quantum sensors are poised to revolutionize the sensing platforms due to their ult ...

EPFL2023

Partial Information Sharing Over Social Learning Networks

Ali H. Sayed, Virginia Bordignon

This work addresses the problem of sharing partial information within social learning strategies. In social learning, agents solve a distributed multiple hypothesis testing problem by performing two operations at each instant: first, agents incorporate inf ...

IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC2023

Results on Sparse Integer Programming and Geometric Independent Sets

Jana Tabea Cslovjecsek

An integer linear program is a problem of the form max{c^T x : Ax=b, x >= 0, x integer}, where A is in Z^(n x m), b in Z^m, and c in Z^n. Solving an integer linear program is NP-hard in general, but there are several assumptions for which it becomes fixed ...

EPFL2023

Byzantine consensus is Θ(n^2): the Dolev-Reischuk bound is tight even in partial synchrony!

Rachid Guerraoui, Seth Gilbert, Vincent Gramoli, Manuel José Ribeiro Vidigueira, Jovan Komatovic, Pierre Philippe Civit

The Dolev-Reischuk bound says that any deterministic Byzantine consensus protocol has (at least) quadratic (in the number of processes) communication complexity in the worst case: given a system with n processes and at most f < n/3 failures, any solution t ...

2023

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

Bayesian reconstruction of memories stored in neural networks from their connectivity

Florent Gérard Krzakala, Lenka Zdeborová

The advent of comprehensive synaptic wiring diagrams of large neural circuits has created the field of connectomics and given rise to a number of open research questions. One such question is whether it is possible to reconstruct the information stored in ...

2023

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

ASSOC COMPUTING MACHINERY2022