Iniciativa IMDEA
Resumen: The Spectre family of speculative execution attacks have required a rethinking of formal methods for security. Approache...
Resumen: Side-channel analysis is one of the main threats against software and hardware implementations of cryptographic algorith...
Resumen: Visibility relations have been proposed by Henzinger et al. as an abstraction for proving linearizability of concurrent ...
Resumen: We provide a simple and efficient in practice algorithm to decide the language inclusion between (nondeterministic) Büch...
Resumen: Bitcoin and many other cryptocurrencies suffer from scalability issues. Payment Channel Networks (PCNs) are the most pro...
Resumen: Refinement types are a type-based, static verification technique designed to be practical. They enrich the types of an e...
Resumen: Private Message Detection (PMD) as a new cryptographic primitive has been identified lately. A PMD protocol aims to allo...
Resumen: Nowadays, computing platforms use a mix of different hardware technologies, as a way to scale application performance, r...
Resumen: Automatic static analysis tools allow inferring properties about software without executing it and without the need for ...
Resumen: Compositionality is a fundamental notion in numerous fields of computer science. This principle can be summarised as fol...
Resumen: Single Secret Leader Election (SSLE) protocols allow a set of users to elect a leader among them so that the identity of...
Resumen: We study the problem of timed asynchronous decentralized monitoring of stream runtime verification specifications. In de...
Resumen: Cloud services improve their availability by replicating data across sites in different geographical regions. A variety ...
Resumen: Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the...
Resumen: We present a novel algorithmic framework to decide whether inclusion holds between ω-regular languages of infinite words...