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