Software Seminar Series (S3)
Tuesday, December 14, 2010
Victor Pablos, Researcher, BABEL, UPMMultivalued and Fuzzy Logic Programming
Abstract: Vague or “fuzzy” concepts appear almost everywhere. The combination of fuzzy logic with logic programming op...
Thursday, December 9, 2010
Alexander Malkis, Researcher, IMDEA Software InstituteS4P - A Practical Generic Privacy Language
Abstract: We present a declarative language with a formal semantics for specifying both users’ privacy preferences and servi...
Wednesday, December 1, 2010
Alexander Malkis, Researcher, IMDEA Software InstituteTutorial rehearsal: Verification of Multithreaded Programs
Abstract: Contents: We give a short survey on the following topics on verification of multithreaded programs: SPIN Specification i...
Tuesday, November 23, 2010
Federico Olmedo, Researcher, IMDEA Software InstituteFormally reasoning about approximate equivalence of probabilistic programs
Abstract: The notion of approximate equivalence of programs plays a fundamental role in several fields of computer science. In par...
Tuesday, November 16, 2010
Santiago Zanella, Researcher, IMDEA Software InstituteA Machine-Checked Formalization of Zero-Knowledge Proofs
Abstract: Zero-knowledge proofs are two-party interactive protocols where one party (the prover) convinces the other one (the veri...
Wednesday, November 10, 2010
Juan Manuel Crespo, Researcher, IMDEA Software InstituteRelational verification using product programs
Abstract: Relational program logics allow reasoning about two programs or two runs of the same program. They provide an elegant me...
Tuesday, November 2, 2010
Marina Egea and Carolina Dania, Researcher, IMDEA Software InstituteMySQL4OCL: A Stored Procedure-Based MySQL Code Generator for OCL
Abstract: In this talk we present a MySQL code generator for OCL expressions which is based on the use of stored procedures for ma...
Tuesday, October 26, 2010
José F. Morales, Researcher, IMDEA Software InstituteA Generator of Efficient Abstract Machine Implementations
Abstract: Implementors of abstract machines face complex, and often interacting, decisions regarding, e.g., data representation, i...
Abstract: “Shared resources” is the term we use to refer to the notation and companion methodology used to teach concu...
Tuesday, September 28, 2010
Boris Köpf, Assistant Research Professor, IMDEA Software InstitutePractical and Provable Security against Side-Channel Attacks
Abstract: Side-channel attacks break cryptosystems by exploiting information that is revealed by the system’s implementation...
Tuesday, September 21, 2010
Klaus Dräger, Researcher, Saarland University, GermanySubsequence Invariants
Abstract: I introduce subsequence invariants, a new class of invariants for the specification and verification of concurrent syste...
Tuesday, September 7, 2010
Alexander Malkis, Post-doctoral Researcher, IMDEA Software InstituteWhat can Owicki-Gries without shared variables prove about resources?
Abstract: Separating data into lock-protected resources is an established paradigm of multi-threaded programming. Programs followi...
Tuesday, July 6, 2010
Álvaro García, Post-doctoral Researcher, IMDEA Software InstituteThe Beta Cube
Abstract: Pure lambda calculus reduction strategies have been thoroughly studied, as they constitute the foundations of evaluation...
Tuesday, June 15, 2010
José Miguel Rojas, PhD Student, The CLIP Laboratory, UPMCompositional CLP-based Test Data Generation for Imperative Languages
Abstract: Glass-box test data generation (TDG) is the process of automatically generating test input data for a program by conside...
Tuesday, June 1, 2010
Alexander Malkis, Post-doctoral Researcher, IMDEA Software InstituteCartesian Abstraction and Verification of Multithreaded Programs
Abstract: We consider the refinement of a static analysis method called thread-modular verification. It was an open question wheth...
Tuesday, May 25, 2010
Miguel Angel García de Dios, PhD Student, IMDEA Software InstituteSSG: Smart & Secure GUI Builder
Abstract: We present a development environment for automatically building smart, security-aware GUIs following a model-based appro...
Tuesday, May 18, 2010
John Gallagher, Researcher, IMDEA Software InstituteConstraint-based abstraction of temporal logic
Abstract: We apply the framework of abstract interpretation to derive an abstract semantic function for the modal μ-calculus. The ...
Tuesday, May 11, 2010
Pedro López-Garcia, Researcher, The CLIP Laboratory, UPMNon-failure analysis for (logic) programs
Abstract: Non-failure analysis aims at inferring that procedure calls in a program will never fail. This type of information has m...
Tuesday, May 4, 2010
Rémy Haemmerlé, Researcher, The CLIP Laboratory, UPMCoinductives Semantics for Constraint Handling Rules
Abstract: Constraint Handling Rules (CHR) is a concurrent committed-choice rule-based programming language introduced in the 1990s...
Tuesday, April 27, 2010
Gilles Barthe, Research Professor, IMDEA Software InstituteCryptography is decidable
Abstract: Cryptography is decidable
Tuesday, April 20, 2010
Alejandro Sanchez, PhD Student, IMDEA Software InstituteTowards Decidability for Concurrent Programs that Manipulate Singly Linked List Datatypes
Abstract: Formal verification of imperative programs provides a high guarantee of software reliability, but it is usually a human ...
Tuesday, April 13, 2010
Dragan Ivanović, Researcher, The CLIP Laboratory, UPMAutomatic derivation of continous-time models for service compositions
Abstract: Service compositions define how serveral Web services (loosely coupled platform independent software components exposed ...
Tuesday, March 30, 2010
Pierre Ganty, Assistant Research Professor, IMDEA Software InstituteAn Abstraction Refinement Approach for Model-Checking
Abstract: Model-checking techniques suffer from the state explosion problem that prevents them to scale up. During the past decade...
Tuesday, March 16, 2010
Laurent Mauborgne, Associate Research Professor, École Normale Supérieure, Paris, FranceModification Shapes
Abstract: A difficult point when verifying heap manipulating programs is to be able to separate precisely the part of the heap tha...
Tuesday, March 9, 2010
Cesar Sanchez, Assistant Research Professor, IMDEA Software Institute and CSICNew Results on Regular Linear Tempora Logic (with a quick intro to Automata, Logic and Games)
Abstract: Regular Linear Temporal Logic (RLTL) is a temporal logic that extends the expressive power of Linear Temporal Logic (LTL...
Tuesday, February 23, 2010
Manuel Hermenegildo, Research Professor and Scientific Director, IMDEA Software InstituteAbstract Interpretation-based Debugging, Verification, Certification, and Optimization in Practice
Abstract: This is a followup to my previous talk on the topic. where I presented the basics of abstract interpretation and of para...
Friday, February 19, 2010
Aleks Nanevski, Assistant Research Professor, IMDEA Software InstituteStructuring the Verification of Heap-Manipulating Programs
Abstract: Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as f...
Tuesday, February 16, 2010
Anindya Banerjee, Research Professor, IMDEA Software InstituteRegion Logic for Local Reasoning about Global Invariants
Abstract: Shared mutable objects pose challenges in reasoning, especially for data abstraction and modularity. We present a logic ...
Tuesday, February 9, 2010
Manuel “Stallman-Dominik” Hermenegildo, Certified Org hacker, IMDEA (Free) SoftwareGetting organized collaboratively with Org
Abstract: What to do when we have an empty slot in our popular Theory lunch series? Respond to the overwhelming popular demand for...