IMDEA Software Institute
Distributed protocols such as Paxos play an important role in many
computer systems. Therefore, a bug in a distributed protocol may have
tremendous effects. Accordingly, a lot of effort has been invested in
verifying such protocols. However, due to the infinite state space
(e.g., unbounded number of nodes, messages) and protocols complexity,
verification is both undecidable and hard in practice. I will describe
a deductive approach for verification of distributed protocols, based
Lucas Kuhring and Zsolt István, researchers at the IMDEA Software Institute, will present a demo "I Can't Believe It's Not (Only) Software! Bionic Distributed Storage for Parquet Files" at the 45th International Conference on Very Large Data Bases (VLDB'19) in Los Angeles, USA.
Like every year, the IMDEA Software Institute publishes its annual report that summarizes in general terms the activity that has been carried out during that period of time.
2018’s edition not only updates relevant content but also design and structure. These efforts have been made to make the document more visual, compelling and easier to read.
Last year the Institute was composed by 62 researchers from 18 different nationalities, of which, 26 were PhD students.
I'll present a study of the rate for continuously non-malleable codes. Such codes allow to encode a message in a way that continuous tampering attacks on the codeword yield a decoded value that is unrelated to the original message.
Everyone has heard about quantum computers and that they will compromise the current Internet security.
Quantum computers use q-bits instead of the classical bits and, therefore,
can represent an exponential number of states at once (this is called quantum superposition).
But, what does that mean? Why some algorithms are dramatically speeded up in this paradigm? Are these computers really as powerful as the media makes us think?
Many micro-architectural attacks rely on the
capability of an attacker to efficiently find small eviction sets:
groups of virtual addresses that map to the same cache set. This
capability has become a decisive primitive for cache sidechannel,
rowhammer, and speculative execution attacks. Despite their importance,
algorithms for finding small eviction sets have not been systematically
studied in the literature.
In this paper, we perform such a systematic study. We begin by
In this talk, we introduce proof-relevant resolution, a framework for constructive proof automation. The intended application of the framework is verifiable proof automation in strongly typed programming languages. We motivate the framework by two use-cases that show its strengths. First, we show a proof-relevant approach to type inference and term synthesis. Secondly, we demonstrate the use of the framework for the purpose of study semantical properties of programming languages, namely soundness of type-class elaboration.