Software Seminar Series (S3)

Abstract: Internet traffic is exposed to potential eavesdroppers. Standard encryption mechanisms do not provide sufficient protect...


Juan Manuel Crespo

Tuesday, December 4, 2012

Juan Manuel Crespo, Post-doctoral Researcher, IMDEA Software Institute

Secure multi-execution through static program transformation

Abstract: Secure multi-execution (SME) is a dynamic technique to ensure secure information flow. In a nutshell, SME enforces secur...


Abstract: Drive-by downloads are the preferred distribution vector for many malware families. In the drive-by ecosystem many explo...


Abstract: RFuzzy framework is a Prolog-based tool for representing and reasoning with fuzzy information. The advantages of our fra...


Raúl Alborodo

Tuesday, November 13, 2012

Raúl Alborodo, Researcher, BABEL, UPM

Making TACO spicy

Abstract: TACO is a tool for formal verification of programs that helps developers find bugs in early stages. TACO translates anno...


François Dupressoir

Tuesday, November 6, 2012

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

Proving Computational Security with a General-Purpose C Verifier

Abstract: Security protocols and APIs are difficult to specify and implement. A reference or prototype implementation written in C...


Maria Garcia de la Banda

Tuesday, October 30, 2012

Maria Garcia de la Banda, Associate Research Professor, Monash University, Australia

Extending Lazy Clause Generation to break symmetries and almost symmetries

Abstract: Lazy Clause Generation is a powerful approach for reducing search in Constraint Programming. It works by recording the r...


Juan Manuel Crespo

Tuesday, October 23, 2012

Juan Manuel Crespo, PhD Student, IMDEA Software Institute

Synthesis of Secure Public-Key Encryption Schemes

Abstract: Program synthesis offers an effective means to exhaustively explore the design space of a class of algorithms: it can se...


Tuesday, October 16, 2012

Diego Esteban Alonso Blas, PhD Student, Universidad Complutense de Madrid, Spain

On the Limits of the Classical Approach to Cost Analysis

Abstract: Static Cost Analysis aims at estimating the amount of resources that an execution of a given program consumes. By resour...


Tuesday, October 9, 2012

Juan Diego Campo, Researcher, Universidad de la República, Udelar, Uruguay

Cache-leakage Resilient OS Isolation in an Idealized Model of Virtualization

Abstract: Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goals is to ...


Peter Stuckey

Tuesday, October 2, 2012

Peter Stuckey, Professor, The University of Melbourne, Australia

Conflict Driven Lazy Decomposition

Abstract: Two competing approaches to handling complex constraints in satisfaction and optimization problems using SAT and LCG/SMT...


Wednesday, June 6, 2012

Abu Nasser Masud, PhD Student, The CLIP Laboratory, UPM

On the Termination of Integer Loops

Abstract: In this talk, I will present our recent study on the decidability of termination of several variants of simple integer l...


Pablo Chico de Guzmán

Tuesday, May 8, 2012

Pablo Chico de Guzmán, PhD Student, IMDEA Software Institute

Tabled Logic Programming and Constraints

Abstract: The evaluation of Prolog, the most successful Logic Programming language, is based on the SLD resolution strategy. SLD p...


Noam Zeilberger

Tuesday, April 24, 2012

Noam Zeilberger, Post-doctoral Researcher, IMDEA Software Institute

Some very preliminary thoughts on zero-knowledge in type theory

Abstract: The notion of “zero-knowledge proof” (an instance of the more general notion of “interactive proof&rdq...


Abstract: Normal order is the standard full-reducing strategy of the pure lambda calculus. It delivers the normal form of a term i...


Ruy Ley-Wild

Wednesday, March 21, 2012

Ruy Ley-Wild, Post-doctoral Researcher, IMDEA Software Institute

Non-Monotonic Self-Adjusting Computation

Abstract: Self-adjusting computation is a language-based approach to writing incremental programs that respond dynamically to inpu...


Abstract: We present an efficient declarative execution mechanism for Logic Programming. Our machine is based on the categorical v...


Boris Köpf

Tuesday, March 6, 2012

Boris Köpf, Assistant Research Professor, IMDEA Software Institute

Automatic Quantification of Cache Side-Channels

Abstract: The latency gap between caches and main memory has been successfully exploited for recovering sensitive input to program...


Ruy Ley-Wild

Tuesday, February 28, 2012

Ruy Ley-Wild, Post-doctoral Researcher, IMDEA Software Institute

Subjective Concurrent Separation Logic

Abstract: From Owicki-Gries’ resource invariants and Jones’ rely/guarantee to modern variants based on separation logi...


Alexander Malkis

Tuesday, February 21, 2012

Alexander Malkis, Post-doctoral Researcher, IMDEA Software Institute

Verification of Software Barriers

Abstract: This poster describes frontiers in verification of the software barrier synchronization primitive. So far most software ...