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