10:45am Lecture hall 1, level B

**Antonio Faonio**, *Post-doctoral Researcher, Instituto IMDEA Software*

Proofs of computational effort were devised to control denial of service attacks. Dwork and Naor (CRYPTO ’92), for example, proposed to use such proofs to discourage spam. The idea is to couple each email message with a proof of work that demonstrates the sender performed some computational task. A proof of work can be either CPU-bound or memory-bound. In a CPU-bound proof, the prover must compute a CPU-intensive function that is easy to check by the verifier. A memory-bound proof, instead, forces the prover to access the main memory several times, effectively replacing CPU cycles with memory accesses. I am going to talk about a new concept dubbed proof of space. To compute such a proof, the prover must use a specified amount of space, i.e., we are not interested in the number of accesses to the main memory (as in memory-bound proof of work) but rather on the amount of actual memory the prover must employ to compute the proof.

**Time and place:**

10:45am Lecture hall 1, level B

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

10:45am Lecture hall 1, level B

**Alvaro Garcia Perez**, *Post-doctoral Researcher, Instituto IMDEA Software*

The Paxos algorithm of Lamport is a classic consensus protocol for state machine replication in environments that admit crash failures. New versions of this protocol are constantly springing that compete with each other for better performance, widening the gap between the description of the Paxos algorithm and the real-world systems. We tackle the challenge of verifying these increasingly complex protocols by applying modular reasoning, this is, by verifying parts of the protocol separately instead of verifying the whole protocol in one go. To this end, we consider the abstractions from an existing decomposition of Paxos by Boichat et al. and we provide highly non-deterministic, atomic specifications of these abstractions that are strong enough to prove the algorithm correct. In this talk I will present our advances in proving that the implementations of Boichat et al. refine (i.e., are linearizable with respect to) our non-deterministic specifications. We conjecture that variants of Paxos and other consensus algorithms, like Multi-Paxos, ZAB and Viewstamped Replication, could be verified in a similar fashion.

**Time and place:**

10:45am Lecture hall 1, level B

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

11:45am Meeting room 202 (*Hill View*), level 2

**Nataliia Stulova**, *PhD Student, Instituto IMDEA Software*

Untyped languages offer great flexibility in term creation and manipulation. To ensure correctness of data operations expensive run-time checks are often used. We propose a simple combination of a strict module system and term hiding mechanism. It allows to make strong assumptions about the shape of the terms in the calls across module boundaries. This in turn leads to significant overhead reductions in the run-time checks, which we demonstrate on a set of benchmarks.

**Time and place:**

11:45am Meeting room 202 (*Hill View*), level 2

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain