Abstract interpretation is a technique which has allowed the development of very powerful program analyzers and transformers, which are at the same time provably correct and highly practical. We will first present the basics of abstract interpretation and of parametric abstract interpretation frameworks (i.e., those in which different abstract domains --analyses-- are "plug-ins"). We will then explore the components of an abstract interpretation-based framework for validating programs with respect to partial specifications written using assertions, detecting and locating bugs, simplifying run-time tests, performing high-level program transformations, and enriching mobile code with certificates.

I will be talking about two main topics. First, on Privacy in Location-aware Services: supplying location-aware services does not necessarily require relinquishing personal (or portable-client) privacy. I will outline an architecture that shows how clients can make choices about how much privacy to give up, while retaining the ability to receive location-aware services. A second topic will be IT for human rights lawyers, or security on the cheap: An organization of human rights lawyers with activities spanning a continent has very demanding security requirements, which must be met with limited resources and facing a broad range of threats. The proposed solution is cheap, proportional to the threats, and incorporates an informal but careful analysis of risks beyond the IT realm. Some considerations include where data should reside, how one prepares to cross a border or leave a computer in a hostile country, how one provides means of secure communication to a party outside the organization.

Several types of parallelism can be exploited in logic programs while preserving correctness and "theoretical efficiency", i.e. ensuring that the parallel execution obtains the same results as the sequential one and the amount of work performed is not greater.In addition to these results, we also have to take into account a number of overheads which appear in practice, such as process creation and scheduling, which can induce a slow-down, or, at least, limit speedup, if they are not controlled in some way. I will talk about a methodology whereby the granularity of parallel tasks, i.e. the work available under them, is efficiently estimated and used to limit parallelism so that the effect of such overheads is controlled.The run-time overhead associated with the approach is usually quite small, since as much work is done at compile time as possible.Also, a number of run-time optimizations are proposed. The performance improvements resulting from the incorporation of grain size control are shown to be quite good, specially for systems with medium to large parallel execution overheads.

Formal verification of imperative programs provides a high guarantee of software quality, but it is usually a human intensive technique. Hence, it is only used in practice for the most critical parts.

Concurrent algorithms are difficult to reason about since their execution consists of different interleavings that may lead to unpredictable and erroneous behaviors. The verification problem becomes particularly challenging when the data structures are dynamic and stored in the heap. Our work focuses on the verification of concurrent data-structures, and the multi-threaded programs that use them. In particular we are interested in verifying general temporal properties. This includes not only safety properties (like invariants) but also liveness properties (like program termination). Our approach differs from most of the currently used techniques in three main aspects:

• First, to reason about data structures allocated on the heap, we employ Regional Logic instead of Separation Logic. This provide us a more expressive and detailed way of describing heap structure thanks to the explicit manipulation of regions of memory.
• Second, our work is based on rely-guarantee reasoning, letting us avoid direct reasoning over all possible thread interleavings. This allows us to describe the visible behavior of all parallel executing threads as a more general rely property, thus simplifying the reasoning problem. Since Regional Logic is a classical (first-order) logic, classical rely-guarantee reasoning can be immediately employed. Moreover, we consider dynamic thread creation.
• Third, instead of reducing the proof of a temporal property to a termination problem and discharging this problem into a termination checker, we make use of general verification diagrams. A verification diagram is a sound and complete method to represent a proof of a general temporal property over a reactive system. The validity check of a verification diagram is reduced to a collection of first-order verification conditions together with a few (decidable) tests over finite graphs.

This Tuesday I will give a brief introduction to the work we have been carrying out along the last months as well as a short explanation of some small working(?) examples on singly-linked concurrent lists that reveals some benefits of the chosen methodologies.

This is joint work with Cesar Sanchez, Anindya Banerjee and Gilles Barthe.

Automatic Generation of Smart, Security-Aware GUI Model Abstract: In many software applications, users access application data using graphical user interfaces (GUIs).There is an important, but little explored, link between visualization and security: when the application data is protected by an access control policy, the GUI should be aware of this and respect this policy. For example, the GUI should not display options to users for actions that they are not authorized to execute on application data.

Directly hardcoding the security policy within the GUI is inadequate.GUI designers are not (and usually should not be) aware of the application data security policy.We propose a solution based on model transformations in a model-driven development setting.We define a many-models-to-model transformation that, given a security-aware data model and a GUI model, makes the GUI model security-aware and also smart. Then, we define a second transformation that, given a security-aware GUI model, also makes this model smart. Smartness is relevant since events can not only trigger actions on application data, but also also on GUI widgets. For example, the resulting GUI widgets will not give users the option to open other widgets when this would allow users to execute unauthorized actions on the application data. Overall, we aim to provide GUI designers with better models and tools for building and analyzing GUIs for security-critical applications.

Comments: on-going work, in collaboration with David Basin (ETH Zürich), Marina Egea (ETH Zürich), and Michael Schläpfer (ETH Zürich).

SecureUML is a modeling language for adding (role-based) access-control requirements to software-system models. SecureUML is designed to be applied in a model-driven software development process, where system-models are typically defined using (various) domain-specific modeling languages. In this talk, I will explain the semantics of SecureUML, and how this semantics can be "plugged" into the semantics of different domain-specific modeling languages.

We present a new algebraic semantics for constraint logic programming based on Freyd's allegories. Our objectives are twofold:

• To build an executable algebraic model for CLP, in the spirit of other algebraic abstract machines.
• To apply existing improvements in categorical semantics to CLP languages.

Starting with Asperti and Martini in 1989, several algebraic models for logic programming have been proposed in the literature. Most of these proposals are based on some form of indexed monoidal categories, already presented at Theory Lunch by James Lipton.

A different proposal using distributive relational algebras was done by Broome and Lipton. The keystone is to interpret predicates as a co-reflexive binary relations. Generalization of this approach to a categorical setting allows us to forget about some of the structure present in the IMC methods, concretely, the indexation functor and the monoidal structure are no longer needed.

In order to build a tabular additive allegory suitable for logic programming, we start with a category and require its HomSets to be equipped with intersection, union, and dual, thus each HomSet becomes a complete lattice. The regular category built from the free Lawvere theory of theprogram's signature becomes an ideal candidate. The translation from logic programs to co-reflexive relations is as follows: predicates are arrows and ∧ is interpreted as arrow composition. This similarity with categorical semantics of other paradigms (think of functional programming) opens up the door to exploring some new constructions over logic programs.

Outline of the talk:

• -Introduction and basic definitions.
• -A Categorical Abstract Machine.
• -Advanced examples: monads, types.

Representing and handling state mutations in Prolog can be cumbersome without resorting to internal database, global variables, or destructive assignment. In standard Prolog, state is usually carried in additional predicate arguments, and the programmer is responsible for manually ensuring threading. Furthermore, such code usually has to be significantly rewritten whenever state structure changes. The result is code that is complicated, error prone, hard to maintain and characterized by a low degree of reuse. These problems make Prolog less appealing for development of complex software systems.

The talk is about the work in progress on extending Prolog with contextual notation and semantics for automatic threading of structured state using source code transformation. We tackle the underlying concepts, rules, techniques, mechanisms and Ciao implementation. We reflect on their relationships with typing, module system, program analysis, and object-oriented programming paradigm.

Abstract machines provide a certain separation between platform-dependent and platform-independent concerns in compilation. Many of the differences between architectures are encapsulated in the specific abstract machine implementation and the bytecode is left largely architecture independent. Taking advantage of this fact, we present a framework for estimating upper and lower bounds on the execution times of logic programs running on a bytecode-based abstract machine.

Our approach includes a one-time, program-independent profiling stage which calculates constants or functions bounding the execution time of each abstract machine instruction.

Then, a compile-time cost estimation phase, using the instruction timing information, infers expressions giving platform-dependent upper and lower bounds on actual execution time as functions of input data sizes for each program.

Working at the abstract machine level allows taking into account low-level issues without having to tailor the analysis for each architecture and platform, and instead only having to redo the calibration step.

Applications of such predicted execution times include debugging/verification of time properties, certification of time properties in mobile code, granularity control in parallel/distributed computing, and resource-oriented specialization.

Formalisms involving some degree of nondeterminism are frequent in computer science. In particular, various programming or specification languages are based on term rewriting systems where confluence is not required. In this talk we will examine three concrete possible semantics for non-determinism that can be assigned to those programs. Two of them –call-time choice and run-time choice– are quite well-known, while the third one –plural semantics– is investigated for the first time in the context of term rewriting based programming languages. We will show some basic intrinsic properties of the semantics and establish some relationships between them: the three semantics form a hierarchy in the sense of set inclusion, and besides call-time choice and plural semantics enjoy a remarkable compositionality property that fails for run-time choice; finally, we will show how to express plural semantics within run-time choice by means of a program transformation, whose adequacy has been formally proved. To conclude, a prototype developed in the Maude system based on the aforementioned transformation and the natural rewriting on-demand evaluation strategy will be also presented.

I will present a simple(!) categorical framework for Logic Programming that gives a syntax, and semantics for logic programs defined over a category. This framework captures constraints, state-change and the use of different logical extensions.The semantics includes generalized "Herbrand-style" interpretations as well as more operational notions of model. A completeness theorem will be sketched using bottom-up semantics and fixed points. I will give some monad examples as well.

The results presented are from a joint paper with Amato and McGrail, joint work in progress with Ed Morehouse, and from earlier work with Krishnan, Freyd and Finkelstein.

Categorical foundations for logic programming started with work by Burstall, Asperti, Corradini, Montanari, Goguen, Power and others. I will briefly sketch the development of some of the main ideas over the years.

While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, there are comparatively fewer proposals that support parallel execution of a sequence of loops or nested loops in the case where such loops have dependencies among them. This work introduces a refined notion of independence, called eventual independence, that in its simplest form considers two loops, say loop1 and loop2 , and captures the idea that for every i there exists k such that the {i + 1}-th iteration of loop2 is independent from the j -th iteration of loop 1, for all j>=k. Eventual independence provides the foundation of a semantics-preserving program transformation, called synchronized pipelining, that makes execution of consecutive or nested loops parallel, relying on a minimal number of synchronization events to ensure semantics preservation.

IMDEA Software has unique oportunities for students that want to get involved in research. The European Master in Computational Logic (EMCL) offers students specialized studies in the uses of logic in computer science, and opens them a venue towards doctoral studies and research. Benefits can thus result from a more tight collaboration between the two entities. Francisco (Paco) is the coordinator of EMCL, and will be presenting the Master, its program structure, collaborations with other universities, and the open possibilities for collaboration with IMDEA.

Model driven development holds the promise of reducing system development time and improving the quality of the resulting products. SecureUML is an expressive UML-based language for constructing security-design models. Security design models are models that combine design specifications with specification of their security policies. The security policies might include both declarative aspects and programmatic aspects. Declarative aspects referred to static access control, like the assignment of users and permissions to roles, while programmatic referred to dynamic information, that is, to the satisfaction of authorization constraints in a given instance of a security-design model.

A formal semantic for the security models has been defined, that allow to make well-defined queries on the security-design models in order understand potentially subtle consequences of the policies they define.

During this talk the Secure UML language will be introduced. Also, using a SecureUML modeling tool that we have developed at IMDEA Software, we will show how security-design models can be specified and, more interestingly, how they can be analyzed in a rigorous and automatic way.

Verification of multi-agent systems is a challenging task due to their dynamic nature, and the complex interactions between agents. An example of such a system is the RoboCup Soccer Simulator, where two teams of eleven independent agents play a game of football against each other. In this talk I will discuss an attempt to verify a number of properties of RoboCup football teams, using a methodology involving testing. To accomplish such testing in an efficient manner we use the McErlang model checker, as it affords precise control of the scheduling of the agents, and provides convenient access to the internal states and actions of the agents of the football team.

Since the mid-90's, the automata techniques have been one of the dominant approaches to temporal verification. In order to check whether program P satisfies temporal specification S, one builds a structure A_P capturing the executions of P, and an automaton A_S capturing the traces allowed by S. This way, the verification problem reduces to check whether A_P ⊂ A_S, or equivalently A_P ∩ (∁ A_S) is empty. The verification problem is then reduced to intersection and complementation of automata.

The classical translations from LTL into w-automata proceeds by first transforming the expression into negation normal form, and then constructing a non-deterministic Büchi automata (NBW). Alternatively, one can use an alternating Büchi automata (ABW), which avoids the state explosion in the construction. However, these approaches are not "algebraic" in the sense the automata is not built from automata for smaller expressions by application of simple automata constructions. Moreover, it only works for logics (LTL) with negation normal forms.

I will justify the advantages of using strong alternating parity automata (APW), and sketch the proof of complexity of the emptyness problem for APW.

I will introduce the necessary concepts from automata theory, game theory and complexity theory, to make the talk as self-contained as possible.

This is joint work with Moshe Vardi and Martin Leucker.

I will briefly explain the basic concepts of functional programming. I will then move on to show you typical examples of pure code in Haskell involving currying, touching on the topic of laziness. Next, I will show you that imperative programming is functional programming with a data structure: the monad. I will illustrate the basic ideas with a simple 6-line program that reads a file and writes a new file with the former's lines sorted. If time permits, I could show you a monadic type-checker for a simple expression language.