Software Seminar Series (S3)

Damir Valput

Tuesday, December 15, 2015

Damir Valput, PhD Student, IMDEA Software Institute

Oscillation Bounded Behaviors for Pushdown Automata

Abstract: I will present a measure, called oscillation, for behaviors of pushdown automata which are finite state automata with au...


Abstract: In this talk, we will present an ongoing effort towards employing a concurrent Separation-style logic (FCSL) for reasoni...


Abstract: Model-driven methodologies can help developers create more reliable software. In previous work, we have advocated a mode...


Abstract: Anonymous communication systems ensure that correspondence between senders and receivers cannot be inferred with certain...


Pablo Cañones

Tuesday, November 17, 2015

Pablo Cañones, PhD Student, IMDEA Software Institute

Security of Cache Replacement Policies

Abstract: Cache memories are an important tool for the good performance of computers since they solve the problem of retrieving da...


Abstract: Security in the Generic Group Model is a standard requirement for new hardness assumptions in (bilinear) groups. Recentl...


Abstract: Cybercriminals use different types of geographically distributed servers to run their operations such as C&C servers...


Abstract: We introduce the notion of asymmetric programmable hash functions (APHFs, for short), which adapts Programmable Hash Fun...


Abstract: We consider the problem of computing a bounded error approximation of the solution over a bounded time [0, T ], of a par...


Irfan Ul Haq

Tuesday, August 4, 2015

Irfan Ul Haq, PhD Student, IMDEA Software Institute

Identifying Undesired Interactions between Variables

Abstract: Interaction between variables, in a program, is a common phenomenon. Sometimes, programmers make a mistake and use varia...


Abstract: Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to aban...


Platon Kotzias

Tuesday, July 21, 2015

Platon Kotzias, PhD Student, IMDEA Software Institute

A Matter of Trust: Malware Abuse in Authenticode Code Signing

Abstract: Code signing is a solution to verify the integrity of software and its publisher’s identity,but it can be abused b...


Benedikt Schmidt

Tuesday, July 14, 2015

Benedikt Schmidt, Post-doctoral Researcher, IMDEA Software Institute

Automated Proofs of Pairing-Based Cryptography

Abstract: Analyzing cryptographic constructions in the computational model, or simply verifying the correctness of security proofs...


Goran Doychev

Wednesday, July 8, 2015

Goran Doychev, PhD Student, IMDEA Software Institute

Rational Protection Against Timing Attacks

Abstract: Provably fixing security problems can make a system unusable, while patching the system to protect from the latest secur...


Artem Khyzha

Tuesday, June 23, 2015

Artem Khyzha, PhD Student, IMDEA Software Institute

A Generic Logic for Proving Linearizability

Abstract: Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms, and recent years ha...


Abstract: In this talk we will review the general resource analysis framework present in the CiaoPP system. We will start by descr...


Alessandra Gorla

Tuesday, June 9, 2015

Alessandra Gorla, Assistant Research Professor, IMDEA Software Institute

An Evolutionary Approach to Unit-Level Invariant Discovery

Abstract: Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting inva...


Alexey Gotsman

Tuesday, June 2, 2015

Alexey Gotsman, Assistant Research Professor, IMDEA Software Institute

Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems

Abstract: To achieve scalability and availability, modern distributed systems often provide only weak guarantees about the consist...


Abstract: Logic programming systems featuring Constraint Logic Programming and tabled execution have been shown to increase the de...


Nataliia Stulova

Tuesday, May 19, 2015

Nataliia Stulova, PhD Student, IMDEA Software Institute

Practical Run-time Checking via Unobtrusive Property Caching

Abstract: Using annotations, referred to as assertions or contracts, to describe program properties for which run-time tests are t...


Abstract: We consider the problem of computing a bounded error ap-proximation of the solution over a bounded time [0, T], of a par...


Dragan Ivanovic

Tuesday, May 5, 2015

Dragan Ivanovic, Post-doctoral Researcher, IMDEA Software Institute

Backtracking, non-determinism, and cuts in F# under 100 lines of code

Abstract: In this talk I’ll try to practically demonstrate how some of the key features of Prolog-style logic programming ca...


Abstract: Anonymity networks such as Tor are a critical privacy-enabling technology. Tor’s hidden services protect the locat...


Pierre Ganty

Tuesday, March 24, 2015

Pierre Ganty, Assistant Research Professor, IMDEA Software Institute

Parameterized Verification of Asynchronous Shared-Memory Systems

Abstract: We study systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes com...


Dario Fiore

Tuesday, March 17, 2015

Dario Fiore, Assistant Research Professor, IMDEA Software Institute

Efficiently Verifiable Computation on Encrypted Data

Abstract: We study the task of verifiable delegation of computation on encrypted data. We improve previous definitions in order to...


Abstract: We introduce a model for mixed syntactic/semantic approximation of programs based on symbolic finite automata (SFA). The...


Ilya Sergey

Tuesday, February 24, 2015

Ilya Sergey, Post-doctoral Researcher, IMDEA Software Institute

Programming and Proving with Fine-Grained Concurrent Resources

Abstract: In the past decade, significant progress has been made towards design and development of efficient fine-grained (i.e., l...


Michael Emmi

Tuesday, February 17, 2015

Michael Emmi, Researcher, IMDEA Software Institute

Checking Observational Refinement, Tractably

Abstract: Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections are essential to moder...


Tuesday, February 10, 2015

Leandro Guillén, Guillermo Jiménez, Project Staff, IMDEA Software Institute

Telefonica-IMDEA JRU working on FIWARE

Abstract: FIWARE is an open platform which integrates advanced OpenStack-based Cloud capabilities and a library of Generic Enabler...


Andrea Cerone

Tuesday, February 3, 2015

Andrea Cerone, Post-doctoral Researcher, IMDEA Software Institute

On Probabilistic, Broadcasting Distributed Systems

Abstract: I propose a process calculus to model high-level distributed systems, whose topology is described by a digraph. The calc...


François Dupressoir

Tuesday, January 27, 2015

François Dupressoir, Post-doctoral Researcher, IMDEA Software Institute

Towards Verifiably-Secure Masking Compilers

Abstract: Masking schemes transform circuits such that even adversaries that may learn the value of some intermediate wires do not...


Alessandra Gorla

Tuesday, January 20, 2015

Alessandra Gorla, Assistant Research Professor, IMDEA Software Institute

Mining Android Apps for Anomalous Behaviors

Abstract: How do we know a program does what it claims to do? In this talk I will present CHABADA, our technique to detect suspici...