IMDEA Software

IMDEA initiative

Home > Events > - Previous Software Seminar Series

Software Seminar Series (S3) - Fall 2009

Álvaro García Pérez

Tuesday, December 15, 2009

Álvaro García Pérez, PhD Student, IMDEA Software Institute

The beta-cube. A space of evaluation strategies for the untyped lambda-calculus


Different evaluation orders for the untyped(1) lambda-calculus exists (call-by-value, call-by-name, normal order, applicative order...), reflecting the nuances in the evaluation of a system which serves as the foundation of functional programming languages.

In this talk, I will introduce a generic evaluator (written in Haskell) which can be instantiated to any evaluator realising a particular evaluation order. For this purpose, I will recall some notions of the untyped lambda-calculus, give an algebraic data type representing lambda-terms, present the big-step semantics of the evaluation orders using natural deduction rules, implement them (using CPS following Reynolds' advice and showing alternative solutions in Haskell), show how monads can help to write neater code, present a way to hybridate existing evaluation orders to produce new ones, comment about an absortion theorem regarding hybridation and describe something I call the "beta-cube".

(1) We prefer to use "untyped" rather than "pure" so as to avoid recent controversy regarding the latter word.

Julian Samborski Forlese

Tuesday, December 1, 2009

Julian Samborski Forlese, PhD Student, IMDEA Software Institute

Dependent Types for Low-Level Programming


Types provide a convenient and accesible mechanism for specifying program invariants. Dependent types extends simple types with the ability to express invariants relating multiple state elements. While such dependencies likely exists in all programs, they play a fundamental role in low-level programming. These dependencies are essential even to prove simple properties like memory safety. In this talk I will present an overview of a type system that combines dependent types and mutation for variables and for heap-allocated structures, and a technique for automatically inferring dependent types.

Note: The talk will be based on the paper Dependent Types for Low-Level Programming by Jeremy Condit, Mathew Harren, Zachary Anderson, David Gay, and George Necula.

Angel Herranz

Tuesday, November 24, 2009

Angel Herranz, Assistant Professor, BABEL, UPM

Validation of UML Models with Uppaal. A Case Study in ERTMS


There is a growing interest in the use of UML for the modeling of embedded and hybrid systems. A key factor for the adoption of model driven methods is the possibility to promptly validate designs and reveal inconsistent and incomplete requirements. But most of the interesting properties to check are beyond the capabilities of common tools. We show a transformation of UML models into Uppaal specifications that can then be used to analyse complex behavioural properties. An industrial case study on the modelling of ERTMS is used to show the applicability of our approach in the detection of property violations.

Tuesday, November 17, 2009

Edison Mera, PhD Student, The CLIP Laboratory, UPM

Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework


We present a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our overall approach is that we preserve the use of a unified assertion language for all of these tasks. We first describe a method for compiling run-time checks for (parts of) assertions which cannot be verified at compile-time via program transformation.

This transformation allows checking preconditions and postconditions, including conditional postconditions, properties at arbitrary program points, and certain computational properties.

The implemented transformation includes several optimizations to reduce run-time overhead. Most importantly, we propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions.

We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO Prolog compliance and to the detection of different types of bugs in the Ciao system source code. We have performed some experiments to assess different trade-offs among program size, running time, or levels of verbosity of the messages shown to the user.

The talk will be divided into two parts. The first one will be devoted to the description of the unified framework, and a demonstration of the system will be performed in the second part.

Juan Manuel Crespo

Tuesday, November 10, 2009

Juan Manuel Crespo, PhD Student, IMDEA Software Institute

Type theory and type conversion


The definition of type equivalence plays a crucial role in any statically typed language. In dependent type theories, there is no syntactic distinction between terms and types, and this notion of equivalence, generally referred to as conversion, is fundamental for typechecking.

Dependent type theories are classified in two categories according to the way in which conversion is handled:

extensional type theories (as implemented in NuPRL) identify conversion with propositional equality (expressed as a type and used for reasoning) resulting in powerful systems with undecidable typechecking;

intensional type theories (as implemented in Coq, Agda and Epigram) use a decidable notion of conversion, typically β-equivalence, and rely on strong normalisation to guarantee decidable typechecking. In the talk we will focus on this class.

The talk will consist of two parts: first I will show that in some cases the notion of conversion present in intesional type theories can be too weak. I will do so through a set of simple practical examples developed in Agda2. In the second part I will informally review some research aimed at extending conversion without compromising decidability of typechecking.

Santiago Romero

Tuesday, November 3, 2009

Santiago Romero, Research Intern, IMDEA Software Institute

Runtime monitoring of asynchronous systems with calls and returns (plus statistical information)


Interest on runtime verification has grown in recent years and a lot of work has been focused on finding suitable formalisms to express the properties to be monitored. Many interesting properties such as correctness of procedures with respect to pre and post conditions and properties on the execution stack cannot be written in plain LTL, and a few alternatives have been presented to achieve it.

In this talk we present LOLA, a simple and expressive specification language that allows statistical information to be gathered along the trace. We also briefly describe the algorithm for online monitoring of asynchronous systems and how we extend this language to specify context and stack sensitive properties. Finally, we show how this extension of LOLA allows interesting properties to be precisely expressed by means of examples.

This is joint work with César Sánchez.

Alan Mycroft

Tuesday, October 27, 2009

Alan Mycroft, Invited researcher, IMDEA Software Institute

Program Testing via Hoare-style Specifications


Program Validation (testing) and Verification (formal proof) are too often seen as disjoint subject areas. We observe that a typical "unit test" (e.g. in JUnit) first creates some data structure, then invokes the procedure under test, then checks an assertion --in essence a Hoare Triple {P}C{Q} but opaquely coded. The Hoare-triple view of tests greatly simplifies the coding of tests, expecially for procedures which mutate data structures or raise exceptions. Such tests can be implemented using transactional memory to provide access to both x and old(x), and for more high-level constructs such as modifiesonly(x.f,y.g). We show how such tests may be compiled into standard Java. Moreover, this view encourages generalised tests in which preconditions can use logical forms such as "forall" and implication. Transactional techniques allow such generalised tests to be used during execution on real data as a form of a test mode. This is joint work with Kathryn Gray, extending FASE'2009 work.

Federico Olmedo

Tuesday, October 13, 2009

Federico Olmedo, PhD Student, IMDEA Software Institute

Provable security of cryptographic schemes


For a long time, the arguments that members of the cryptographic community used to exhibit in favor of the security of cryptosystems were deficient and weak (eg empiric validations, wrong proofs). On the contrary, provable security aims to provide the users with more rigorous arguments in favor of cryptographic schemes' security.

The concept of provable security was introduced by Goldwasser and Micali in their seminar paper Probabilistic Encryption in 1984. It heavily relies on the "computational model". In this talk we will present the computational model of security and the keys ideas underlaying provable security. This encompasses describing the sort of attackers it considers, how "security" is broadly defined and which proof techniques are used. Regarding proof methodologies, we will specially focus on the "game-playing" technique and (if not running out of time) we will present a proof of ElGamal IN-CPA security using this framework.

Tuesday, October 6, 2009

Pedro R. D'Argenio, Professor, FaMAF, Universidad Nacional de Córdoba - CONICET, Argentina

Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers


The technique of partial order reduction (POR) for probabilistic model checking prunes the state space of the model so that a maximizing scheduler and a minimizing one persist in the reduced system. This technique extends Peled's original restrictions with a new one specially tailored to deal with probabilities.

It has been argued that not all schedulers provide appropriate resolutions of nondeterminism and they yield overly safe answers on systems of distributed nature or that partially hide information. In this setting, maximum and minimum probabilities are obtained considering only the subset of so-called distributed or partial information schedulers.

In this article we revise the technique of partial order reduction (POR) for LTL properties applied to probabilistic model checking. Our reduction ensures that distributed schedulers are preserved. We focus on two classes of distributed schedulers and show that Peled's restrictions are valid whenever schedulers use only local information. We show experimental results in which the elimination of the extra restriction leads to significant improvements.

Juan Cespedes

Tuesday, September 29, 2009

Juan Cespedes, System Administrator and Developer, IMDEA Software Institute

Foundations of Dynamic Tracing


In this talk I will present the first principles of dynamic tracing, in particular tracing of systems programs. Tracing is used for building debuggers, monitors and runtime-verification tools.

I will start by introducing the support that modern processors and operatings offer for tracing, focusing on the facilities exposed by the Linux kernel. Then, I will describe how a dynamic library tracer can be built using this infrastructure. The paramount example is the tool ltrace which I implemented a while ago.

Finally, I will describe the changes required to extend a dynamic library tracer into a runtime-verification infrastructure that handles concurrency (both light and heavy threads, both simulated concurrency and real-multicore multi-processors). Bagheera is a toolkit being developed at IMDEA-Software that implements these extensions and is reprogammable.

Bagheera is joint work with Santiago Romero and Cesar Sanchez.

Software Seminar Series (S3) - Spring 2009