Alvaro Garcia, PhD Student, IMDEA Software Institute
Gradual typing aims at combining static and dynamic type checking by introducing a dynamic type and cast expressions. The dynamic type is assigned to expressions whose type is unknown until run time. A typed-based cast expression <S<=T>^l e specifies that the value of expression e is to be coerced form type T to S at run time. If such a coercion cannot be performed, the cast fails returning the blame label l. Recent works on the area deal with the dynamic semantics of gradual typing, where the choice of error-detection policy (eager or lazy) and of blame-tracking strategy (upcast-downcast or downcast), as well as the space efficiency issues make up a rich design space for dynamically typed lambda calculi with higher-order casts (Siek et al. 2009).
The gradually-typed lambda calculus is a version of the simply-typed lambda calculus with higher-order casts and blame labels. Henglein's coercion calculus (Henglein 1993) underlies the casts in the gradually-typed lambda calculus. Coercions consist of some atomic operations that can be composed in a sequence or in an arrow. The coercion contraction rules specify how to reduce coercions, obtaining a normal coercion.
We establish by program transformation the correspondence between the reduction semantics of a closure-converted gradually-typed lambda calculus and the definitional interpreters presented by Siek and García. Thus we prove, for the case of the eager error-detection policy and the downcast blame-tracking strategy, Siek and Garcia's conjectures concerning the correctness of their interpretation with respect to the calculus. The proof of correctness is easily generalised for other choices of error-detection policies and blame-tracking strategies by plugging a different set of coercion contraction rules at the start of the derivation.
This is joint work with Ilya Sergei and Pablo Nogueira.
Miriam García, PhD Student, IMDEA Software Institute
This talk will introduce a novel abstraction technique and a model checking algorithm for analysing stability of a particular class of hybrid systems. Hybrid systems are physical systems evolving in time, which exhibits a mixed discrete and continuous behaviour. Stability is a control design property establishing that small perturbations on the input just induce small changes on the output.
The proposed technique consists of defining a simple system, an abstraction, from an initial hybrid system, and applying a model checking algorithm to determine stability. The proposed abstraction procedure is a modified predicate abstraction, which gives an abstract weighted graph. Model checking consists of analysing the finite weighted graph for the absence of certain kinds of cycles which can be solved by dynamic programming. It is shown that the abstraction is sound in that a positive result on the analysis of the graph implies that the original system is stable.
The feasibility of the approach has been demonstrated by a prototype implementation.
Juan Manuel Crespo, PhD Student, IMDEA Software Institute
EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.
This talk will consist of two parts. I will begin by introducing some standard notions used in cryptography and I will show how they are modelled using Easycrypt. I will then develop an Easycrypt proof of security under chosen plaintext-attacks of a simple encryption scheme introduced by Bellare and Rogaway in 1993. While straightforward, this proof exhibits some of the fundamental reasoning patterns used pervasively in cryptographic proofs.
Dragan Ivanović, Post-doctoral Researcher, IMDEA Software Institute
Constraint and logic programming languages offer programmers powerful, declarative ways to go about solving complex computational problems that involve logical reasoning in one form or another. In particular, the Constraint Handling Rules (CHR) have been developed as a language for developing constraint solvers. CHR can be seen as a language parametric relative to an underlying host programming language of choice. While CHR traditionally integrates well with Prolog, its integration with the mainstream languages such as Java is much less smooth, and the support for IDEs and debugging practically non-existent. Yet writing solvers in Prolog/CHR and then interfacing them with Java is not really an option if one wants to populate the universe of discourse with complex Java objects whose implementations we don't know and reason directly on them.
In this talk I shall present a general-purpose Java library that I developed for the purpose of writing CHR-style constraint solvers and reactive rule / event processing programs directly in Java, without another language layer. The CHR-style rules are written in a subset of Java, and are easily amenable to the usual code refactoring tools found in modern IDEs such as Eclipse, NetBeans, or IntelliJ/IDEA. Two additional orthogonal features are the ability to save/restore the state of the constraint store, and the event notification system that allows us to distribute events and helps us build console-based and visual debuggers.
Germán Delbianco, PhD Student, IMDEA Software Institute
Continuations are programming abstractions that allow for manipulating the "future" of a computation. Amongst their many applications, they enable implementing unstructured program flow through higher-order control operators such as the callcc operator of your functional programming language of choice.
In this talk we present HTTcc, a Hoare-style logic for the verification of programs with higher-order control, in the presence of mutable dynamic state. This is done by designing a dependent type theory with first class callcc and abort operators, where pre- and postconditions of programs are tracked through dependent types. Our operators are algebraic in the sense of Plotkin and Power, to reduce the annotation burden and enable verification by symbolic evaluation.
As a roadmap for this talk, we illustrate working with HTTcc by means of the verification of a couple of non-trivial examples.
Anindya Banerjee, Research Professor, IMDEA Software Institute
When the representation of a data structure changes we would expect that the behaviour of clients using the data structure remains "the same", provided that the data structure is fully encapsulated.
How do we demonstrate such representation independence? This unpolished talk will describe work in progress.
Murdoch Gabbay, Researcher, Heriot-Watt University, United Kingdom
By my understanding, IMDEA works a lot on verification and checking. Iwill sketchnominal techniques and recent activity in the field, and speculate on how nominal techniques could be useful here, with a particular emphasis on why trying to do this might be useful. This talk will be aimed at everybody, especially those who are *not* familiar with nominal techniques. Further reading is (as always) on my webpage.
Murdoch Gabbay, Researcher, Heriot-Watt University, United Kingdom
Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via the Curry-Howard correspondence on an extension of the modal logic S4 with multiple modalities, one for each variable. The application is to meta-programming, where the intuitive denotation of Box A is "syntax of type A".
The language itself is pretty, and we developed a denotational semantics for this which is quite attractive and displays some interesting properties. I will give a tour of the system and discuss future work. The associated journal paper on "Denotations of CMTT" is online.
Zhoulai Fu, PhD Student, INRIA
Strong update — the assignments overwrite the contents of the target property, is essential for precise static analysis of memory operations. Classically, the strong update is safe if such assignment will definitely occur and that it assigns to a unique location.
We find that this classic safety condition of strong update can be weakened if we semantically restrict our analysis to a limited scope of program identifiers, which we will call "targets" in this work. This finding allows us to systematically discover more strong update cases by picking up the appropriate targets.
Our experimental results confirm this finding. In our earlier work, we have developed a static analysis that is able to infer numerical properties for large-scale Java programs. The analysis introduces symbolic variables upon which the "weak update" has to be applied in the classical sense so that the underlined locations reflected by these symbolic variables potentially retain its old values. By selecting as the targets the program identifiers that are used literally in program, we are able to apply "strong update" in many cases where such abstraction is unsafe in the classic sense.
Alejandro Serrano, PhD Student, IMDEA Software Institute
Resource analysis aims to derive tight bounds on the usage of some numerical property. It is instrumental in a wide range of program transformations, including granularity control for parallel and distributed computing, and energy optimizations in embedded systems. In this talk we give an overview of the current state of the art in resource analysis, including the most widely used approaches to it: instrumented interpreters, potential method and recurrence posing. In many of these approaches a initial size analysis, which derives bounds on the size of terms in a program, is run. We look at size analysis using recurrences, the problems with this approach, and propose a solution in terms of sized types. Sized types allow to encode information about subterms in any position and depth, and gives raise to a more precise resource analysis.
Pavithra Prabhakar, Assistant Research Professor, IMDEA Software Institute
Hybrid systems refer to systems exhibiting mixed discrete-continuous behaviors and arise as a natural byproduct of the interaction of embedded processors with physical systems. In this talk, we focus on the verification of a class of properties of hybrid systems called stability. Stability captures the notion that small perturbations to the initial state or input to the system result in only small changes in the eventual behavior of the system. It is a fundamental requirement of any control system design. We present a first result on the decidability/undecidability boundary of stability verification of hybrid systems. Then, as a basis for developing approximation techniques, we present preorders between systems which preserve stability.
Shiva Shabaninejad, Research Intern, IMDEA Software Institute
Modern object oriented languages like C# and JAVA enable developers to build complex application in less time. These languages are based on selecting heap allocated pass-by-reference objects for user defined data structures. This simplifies programming by automatically managing memory allocation and deallocation in conjunction with automated garbage collection.
This simplification of programming comes at the cost of performance. Using pass-by-reference objects instead of lighter weight pass-by value structs can have memory impact in some cases.
These costs can be critical when these application runs on limited resource environments such as mobile devices and cloud computing systems. We explore the problem by using the simple and uniform memory model to improve the performance. In this work we address this problem by providing an automated and sounds static conversion analysis which identifies if a by reference type can be safely converted to a by value type where the conversion may result in performance improvements. This work focuses on C# programs. Our approach is based on a combination of syntactic and semantic checks to identify classes that are safe to convert. We evaluate the effectiveness of our work in identifying convertible types and impact of this transformation.
The result shows that the transformation of reference type to value type can have substantial performance impact in practice. In our case studies we optimize the performance in Barnes-Hut program which shows total memory allocation decreased by 93% and execution time also reduced by 15%.
Julio Mariño, Researcher, BABEL, UPM
In many software projects quality assurance relies largely on testing. Often, this activity is performed in a crafty way, and assigned to personnel with low qualification. There are even some trendy methodologies that advocate the replacement of specifications by the testing code itself. It comes as no surprise that this prevalence of testing may be perceived as one of the main obstacles to the introduction of formal techniques in mainstream software development.
However, there is a growing interest in reconciling formality in software development with the testing activity, resulting in a variant of lightweight formal methods called property-based testing. In this approach, testing code is automatically generated from specifications rather than crafted by hand.
The talk will deal with the relationship between properties -- and, more specifically, types -- with testing code. A series of simple examples will be used to present the technology available and, also, some challenging issues in this strange marriage.
Ilya Sergey, Post-doctoral Researcher, IMDEA Software Institute
In this informal two-part talk I will present recent studies on systematic construction of control-flow analyses for higher-order languages by means of abstract interpretation.
In the first part of the talk, I will give a tutorial on turning a small-step abstract machine into an abstract interpreter, delivering the flows-to information by approximating collecting semantics of a program. The key idea of the approach is eliminating circular dependencies in a semantic state-space and then bounding it by providing an abstraction over its leaf elements. I will also briefly describe advanced techniques, allowing one to improve precision and complexity boundaries of the analysis: widening, abstract garbage collection and counting.
The second part of the talk is more of implementation flavour. Following the same story line, I show a systematic method for transforming a concrete semantics into a monadically-parameterized abstract machine, such that changing the monad changes the behaviour of the machine. By changing the monad, we can recover a spectrum of machines - from the original concrete semantics to a monovariant, flow- and context-insensitive static analysis with a singly-threaded heap and weak updates. The monadic parameterization also suggests an abstraction over the ubiquitous monotone fixed-point computation found in static analysis. This abstraction makes it straightforward to instrument an analysis with high-level strategies for improving precision and performance, such as abstract garbage collection and widening.
Zhoulai Fu, PhD Student, INRIA
In 1978, Cousot and Halbwachs showed how to determine at compile-time linear relations among program variables. Various abstract domains were then introduced to statically infer program numeric properties. Unfortunately, none of these abstract domains are easily applicable to programs with pointers. We propose a framework that combines existing numeric analyses and pointer analyses in a black-box way. This is meaningful: the correction of our approach is guaranteed by construction, and the implementation is easy. We have prototyped this approach using SOOT framework as pointer analyses and PPL library as numeric domains. Tested on Dacapo-2006's benchmarks, the analysis discovers more numeric properties, and scales up to large programs such as ECLIPSE.
At the end of this presentation, I will give a demonstration of the prototype.
Cesar Sanchez, Assistant Research Professor, IMDEA Software Institute
Regular Expressions (RE) are an algebraic formalism for expressing regular languages, widely used in string search and as a specification language in verification. In this work we investigate Visibly Rational Expressions (VRE), an extension of RE for the well-known class of Visibly Pushdown Languages (VPL), a particularly well-behaved class of context free languages.
I will, on demand and in an informal style, show some of the most relevant results:
This is joint work with Laura Bozzelli.
Alejandro Sanchez, PhD Student, IMDEA Software Institute
We study the verification of safety properties over symmetric parametrized systems. These systems consist on an arbitrary and unbounded number of threads running the same program. In this scenario, following standard deductive techniques leads to the need of verifying an unbounded collection of verification conditions which grows with the number of threads involved in the system. To handle this problem, we present a technique based on parametrized invariance rules to reduce the verification of finite and infinite state parametrized programs to the analysis of only a finite number of verification conditions. In our approach, all necessary VCs are automatically generated from the program and its specification, independently of the number of threads involved in the system.
In this talk, we present the latest advances in our research as well as some running examples including a ticket-based mutual exclusion algorithm and a concurrent single-linked list implementation. Both examples are verified using Leap. Leap is a tool under development at the IMDEA Software Institute which implements the parametrized invariance rules. Our tool is able to automatically generate all necessary VCs starting from the program and the properties specifications. Leap also implements decision procedures to automatically verify VCs, and is also extended to interactively assist the user in the verification process. Currently, the decision procedures allow to programs that manipulate numbers, sets, list layouts and their combinations, built on top of state-of-the-art SMT solvers.
This is joint work with César Sánchez.
Alexey Gotsman, Assistant Research Professor, IMDEA Software Institute
Modern geo-replicated databases underlying large-scale Internet services guarantee immediate availability and tolerate network partitions at the expense of providing only weak forms of consistency, commonly dubbed eventual consistency. At the moment there is a lot of confusion about the semantics of eventual consistency, as different systems implement it with different sets of features and in subtly different forms, stated either informally or using disparate and low-level formalisms.
We address this problem by proposing a framework for formal and declarative specification of the semantics of eventually consistent systems using axioms. Our framework is fully customisable: by varying the set of axioms, we can rigorously define the semantics of systems that combine any subset of typical guarantees or features, including conflict resolution policies, session guarantees, causality guarantees, multiple consistency levels and transactions. We prove that our specifications are validated by an example abstract implementation, based on algorithms used in real-world systems. These results demonstrate that our framework provides system architects with a tool for exploring the design space, and lays the foundation for formal reasoning about eventually consistent systems.
This is joint work with Sebastian Burckhardt (Microsoft Research) and Hongseok Yang (University of Oxford).