10:45am Lecture hall 1, level B

**Jesús Domínguez**, *PhD Student, Instituto IMDEA Software*

The Knaster-Tarski Lemma is one of the main tools for obtaining fixpoints. There are also iterative methods, and these allow a translation into Category Theory. In Category Theory, instead of talking about the least fixpoint of a monotone function, we talk about the initial algebra of a functor. Does the Knaster-Tarski Lemma allow a similar translation into the language of algebras, as iterative approaches do? In this talk I will explore an attempt of translation.

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

**Joaquín Arias**, *PhD Student, Instituto IMDEA Software*

Extending ASP with constraints (CASP) enhances its expressiveness and performance. This extension is not straightforward as the grounding phase, present in most ASP systems, removes variables and the links among them, and also causes a combinatorial explosion in the size of the program. Several methods to overcome this issue have been devised: restricting the constraint domains (e.g., discrete instead of dense), or the type (or number) of models that can be returned. In this paper we propose to incorporate constraints into s(ASP), a goal-directed, top-down execution model which implements ASP while retaining logical variables both during execution and in the answer sets. The resulting model, s(CASP), can constrain variables that, as in CLP, are kept during the execution and in the answer sets. s(CASP) inherits and generalizes the execution model of s(ASP) and is parametric w.r.t. the constraint solver. We describe this novel execution model and show through several examples the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other CASP systems. We also report improved performance w.r.t. other very mature, highly optimized ASP systems in some benchmarks.

**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 Meeting room 302 (*Mountain View*), level 3

**Luis Miguel Danielsson**, *PhD Student, Instituto IMDEA Software*

Stream Runtime Verification (SRV) is a behavioral specification language for runtime verification, where a monitor is described by expressing the dependencies between the output streams of values in terms of the input streams of observations. SRV is based on the observation that many monitoring algorithms can be generalized from Booleans to rich data domains. Stream runtime verification provides a friendly language (with a programming look and feel) to express these dependencies and automatically generate monitors that compute the specification. Also, SRV benefits from simplifiers that rewrite expressions maintaining term equivalence. In this presentation I will introduce how to extend SRV for a decentralized setting. The proposed algorithm is suitable for arbitrary connected topologies where a global clock or a synchronization mechanism can be assumed. I will also present advanced communication strategies that help tailoring the resource consumption of the algorithm to the task at hand. Finally I will present empirical results that confirm the adequacy of this approach.

**Time and place:**

10:45am Meeting room 302 (*Mountain View*), level 3

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

10:45am Lecture hall 1, level B

**Felipe Gorostiaga**, *PhD Student, Instituto IMDEA Software*

Stream Runtime Verification (SRV) is a specification formalism for temporal properties of reactive systems where observations are described as streams of data computed from input streams of data, which allows a clean separation between the temporal dependencies between incoming events, and the concrete operations that are performed during the monitoring. However, Stream Runtime Verification languages typically assume that all streams share a global synchronous clock and input events arrive in a synchronous manner. We generalize the time assumption to cover streams whose events are stamped from a real-time domain, but keep the essential explicit time dependencies present in previous synchronous SRV languages. In this talk I will present Striver, a formalism which shares the simplicity with SRV, mainly due to the separation between the timing reasoning and the data domain.

**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 Meeting room 302 (*Mountain View*), level 3

**Isabel García**, *PhD Student, Instituto IMDEA Software*

Approximations during program analysis are a necessary evil, as they ensure essential properties, such as analysis soundness and termination, but they also imply that the analysis is not guaranteed to always produce useful results. In such cases it is necessary to have some means for users to provide information to guide analysis and thus to improve precision, such as the trust assertions of CiaoPP or the "known facts" of Astrée. This allows dealing with, e.g., predicates for which the analysis is not complete or when the source is only partially available. We present techniques for supporting within an abstract interpretation framework with a rich set of trust assertions (conditional, dealing with call/success pairs and multivariance). We extend the language of program-point assertions to deal with multi-variance. Our techniques can also deal with the cases where run-time checks for assertions are present in the program and those in which no run-time checks are generated. Finally, we show how the approach can be applied to both improving precision and accelerating.

**Time and place:**

10:45am Meeting room 302 (*Mountain View*), level 3

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

10:45am Lecture hall 1, level B

**Alejandro Aguirre**, *PhD Student, Instituto IMDEA Software*

A program that computes on an infinite data structure, such as an infinite list or tree cannot be expected to terminate. But for it to behave properly, not only it must run forever, it also must compute arbitrarily precise approximations of the result in finite time. This property is known as productivity, and is the dual of termination. Productivity is well-known and has been studied in a deterministic setting. However, extending it to a probabilistic setting poses some formal challenges. In this talk I will introduce a probabilistic extension of productivity , which we name Almost Sure Productivity (ASP). I will first look further into this duality between termination and productivity, which is essentially the duality between algebras and coalgebras, and present the theoretical background that will allow us to formalize the concept of ASP. Then I will define a core language for probabilistic computations on infinite lists and trees, and provide two methods for checking whether a program is ASP: an efficient but incomplete syntactic criterion, and a decision procedure based on model-checking probabilistic pushdown automata.

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

**Miguel Ambrona**, *PhD Student, Instituto IMDEA Software*

Prime numbers are essential in cryptography. Many cryptographic primitives (RSA encryption, ElGamal, digital signatures...) rely on finding and using large prime numbers (in the range of 256-2048 bits long). But, why are prime numbers important for cryptography? And, how can we check whether such large numbers are prime? In this talk, I will present different techniques to assure primality, such as probabilistic algorithms (that assure with very high probability that the number is prime) and the celebrated AKS algorithm (which is the first known deterministic algorithm for primality checking running in polynomial time). These algorithms are efficient enough to be used in actual cryptographic applications. Additionally, I will talk about the largest prime numbers known by humanity and how we know they are prime (note that the mentioned algorithms cannot be used to assure primality of these staggering numbers and dedicated algorithms must be employed).

**Time and place:**

10:45am Lecture hall 1, level B

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain

12:00pm Meeting room 302 (*Mountain View*), level 3

**Pepe Vila**, *PhD Student, Instituto IMDEA Software*

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 talk, we perform such a systematic study. We begin by formalizing the problem and analyzing the probability that a set of random virtual addresses is evicting. We then present novel algorithms, based on ideas from threshold group testing, that reduce random eviction sets to their minimal core in linear time, improving over the quadratic state-of-the-art. We complement the theoretical analysis of our algorithms with a rigorous empirical evaluation in which we identify and isolate factors that affect their reliability in practice, such as adaptive replacement strategies and TLB thrashing. Our results indicate that our algorithms enable finding small eviction sets much faster than before, and under conditions where this was previously deemed impractical.

**Time and place:**

12:00pm Meeting room 302 (*Mountain View*), level 3

IMDEA Software Institute, Campus de Montegancedo

28223-Pozuelo de Alarcón, Madrid, Spain