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