Abstract: We study implementations of basic fault-tolerant primitives, such as consensus and registers, in message-passing systems...

Abstract: In this talk I will present two algorithms to decide the language inclusion problem between Büchi automata. Our approach...

Abstract: Microarchitectural attacks, such as Spectre and Meltdown, illustrate that artifacts of hardware implementations (like sp...

Abstract: Vector Commitments allow one to (concisely) commit to a vector of messages so that one can later (concisely) open the co...

Abstract: Cryptographic accumulators are a common solution to proving information about a large set . They allow to compute a shor...

Abstract: Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization...

Abstract: Cloud computing has revolutionized the access to and the use of emerging computing hardware technologies. To achieve eff...

Abstract: Proofs of Retrievability (PoRs) are protocols which allow a client to store data remotely and to efficiently ensure, via...

Abstract: Cybercriminals often leverage Bitcoin for their illicit activities. In this work, we propose back-and-forth exploration,...

Abstract: The Spectre family of speculative execution attacks have required a rethinking of formal methods for security. Approache...