Home > Taxonomy > Term > IMDEA Software Institute

IMDEA Software Institute

Fractal Small: 
Fractal Large: 

Talk by Mooly Sagiv: Deductive verification of distributed protocols in first-order logic

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

The Demo by Lucas Kuhring and Zsolt István on "Bionic Distributed Storage for Parquet Files", accepted at VLDB'19

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.

2018’s Annual Report has been published

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.

Talk by Miguel Ambrona & Ignacio Fábregas: Quantum computers: invest wisely, invest in the future!

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?

Talk by Pepe Vila: Theory and Practice of Finding Eviction Sets

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

Talk by František Farka: Proof-Relevant Resolution: The Foundations of Constructive Automation

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.


Subscribe to RSS - IMDEA Software Institute