Totally ordered shared logs have become a key component in modern distributed systems, serving as a building block to ensure consistent execution of operations across replicas and partitions. A key challenge in designing this type of systems is to achieve low latency appends, given that total order requires coordination among participants and, in most designs, this coordination is in the critical path of the application. We present a novel design that removes coordination from the critical path, allowing appends to the log to be executed with low latency. We first discuss how this can be achieved in a single datacenter and, subsequently, we introduce a novel technique that allows the same principles to be applied in partially-replicated geo-distributed logs.This talk presents joint work performed by R. Soares (U. Lisboa), L. Rodrigues (U. Lisboa), R. van Renesse (Cornell U.) and L. Alvisi (Cornell U.).

Decentralized Finance (DeFi) leverages blockchain technology to provide financial services without intermediaries, relying on smart contracts to automate economic transactions. As of October 2025, DeFi protocols are estimated to manage over $100 billion in Total Value Locked, making them ideal targets for attacks. The complexity of DeFi protocols’ incentive mechanisms, combined with their entanglement in low-level implementation details, makes it challenging to precisely assess their structural and economic properties, analyse user strategies and attacks, and ensure that the code accurately reflects the intended functionalities. In this talk, we provide an overview of the different approaches used to study DeFi protocols - ranging from formal models to verification tools, as well as LLM-based methods - outline the main challenges, and discuss future directions.

I will present Zinc, a proof system that addresses the problem of high arithmetization costs in proof systems. Arithmetization is the step where one turns the computation/relation one wants to prove into a constraint that is in a suitable form for the proof system. In many natural applications this step is very costly, in the sense that the final constraints is easily of ‘size’ 16x or 32x than the original computation. Such applications include: hash computations, CPU instructions (arithmetic modulo 2^n and bitwise operations), lattice-based operations (as in, e.g. vFHE operations), legacy cryptography, machine learning, etc. Zinc (https://eprint.iacr.org/2025/316) is a proof system for constraints expressed over the integers. These, as we will see, allow to arithmetize many of the above operations cheaply. Additionally, for the same number of constraints, Zinc’s running time is similar to current state-of-the-art hash based proof system.I will also discuss our ongoing work towards a proof system where all the above operations are cheaply arithmetizable. During the talk I will focus especially on the problem of proving lattice-based operations, with a view of applying our techniques to vFHE

In this talk we present a variant of vertex cover on temporal graphs that has been recently introduced for timeline activities summarization in social networks. The problem has been proved to be NP-hard, even in restricted cases. We present algorithmic contributions for the problem. First, we present an approximation algorithm of factor O(T log n), on a temporal graph of T timestamps and n vertices. Then, we consider the restriction where at most one temporal edge is defined in each timestamp. For this restriction, which has been recently shown to be NP-hard, we present a 4(T-1) approximation algorithm and a parameterized algorithm when the parameter is the cost (called span) of the solution.Joint work with Riccardo Dondi

Modern systems face security challenges at every layer of the stack, from user authentication to machine learning and software execution. In this talk, we present three lines of research aimed at strengthening defenses. First, we discuss advances in password deception, including honeyword generation and breach detection frameworks that address practical weaknesses in existing approaches. Next, we examine the security of machine learning-based services, highlighting vulnerabilities such as membership inference, model inversion, and adversarial text generation, and analyzing why many attacks fail in realistic settings. Finally, we introduce VALIDATE, a novel framework for binary-level security assurance, designed to ensure that applications compiled with memory-safe programming languages (e.g., Rust) retain their protective checks and remain tamper-free before execution. Together, these perspectives underscore the need for holistic, multi-layered security that anticipates and disrupts adversaries at multiple points of attack.