Almost-Invariants: From Bugs in Distributed Systems to Invariants
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.
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 ...
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 ...
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 ...
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 ...
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
Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...
Molecular simulations allow to investigate the behaviour of materials at the atomistic level, shedding light on phenomena that cannot be directly observed in experiments. Accurate results can be obtained with ab initio methods, while simulations of large-s ...
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 ...
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 ...
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 ...
