Iniciativa IMDEA
Resumen: In this talk, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans,...
Resumen: A key aspect of the adoption of blockchain technologies is their performance. Consequently, many techniques to improve t...
Resumen: Abstract interpretation provides an over-approximation of program behaviours that is used to prove the absence of bugs. ...
Resumen: Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) le...
Resumen: We study implementations of basic fault-tolerant primitives, such as consensus and registers, in message-passing systems...
Resumen: In this talk I will present two algorithms to decide the language inclusion problem between Büchi automata. Our approach...
Resumen: Microarchitectural attacks, such as Spectre and Meltdown, illustrate that artifacts of hardware implementations (like sp...
Resumen: Vector Commitments allow one to (concisely) commit to a vector of messages so that one can later (concisely) open the co...
Resumen: Cryptographic accumulators are a common solution to proving information about a large set . They allow to compute a shor...
Resumen: Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization...
