If you have questions please contact the co-chairs of the organizing committee.

Click here for copyright details.

As a satellite event of WoLLIC 2012 a meeting of INFINIS French-Argentinean Laboratory will be hosted on Friday, September 7th.
INFINIS is a French-Argentinean Laboratory (*Laboratoire Internationale Associé*) between *Centre National de la Recherche Scientifique* (CNRS) and * Université Paris Diderot, *on the one hand, and *Consejo Nacional de Investigaciones Científicas y Técnicas* (CONICET) and the *Universidad de Buenos Aires*, on the other. It is devoted to research in Computer Science. Specific focus is placed on formal methods, for modeling, verification and development of complex software artifacts.

The meeting will take place at **Aula 7** of the Departamanto de Computación (Pabellón I, Ciudad Universidaria), of the Facultad de Ciencias Exactas y Naturales, de la Universidad de Buenos Aires, from 9am to 14am on September 7th.

We will explain the algebraic point of view and we will focus on the class of languages recognized by finite groups. It is known that two languages are separable by a group language if and only if their closures in the free group, with respect to the Hall topology, are disjoint.

We exploit this in order to obtain a separating group language in an algorithmic fashion. In [Aui05], a proof is given for the Ribes and Zaleski product theorem. We show that this proof can be converted into a construction giving such a separating group language.

References: [Aui05] B. Auinger, K. Steinberg. A constructive version of the Ribes-Zalesski product theorem. Mathematische Zeitschrift, 250(2):287–297, 2005.

We also give a new tight upper bound for the length of the longest con- trolled descending sequence of multisets of Nn , and use it to give an upper bound for the length of controlled bad sequences in the majoring order- ing of sets of tuples. We apply this upper bound to obtain complexity upper bounds for decision procedures of automata over data trees. In both cases the idea is to linearize bad sequences, i.e. transform them into a descending one over a well-order for which upper bounds can be more easily handled.

This talk focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for Lambda Calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of *necessary set of redexes*, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.

This is joint work with with Eduardo Bonelli, Delia Kesner and Alejandro Ríos and was presented at RTA 2012.

- Non-deterministic finite automata
- k-counter real time non-deterministic finite automata
- Two-way deterministic finite automata

This is joint work with Verónica Becher and Olivier Carton.

This is joint work with Pablo Heiber and Theodore Slaman.

We study dynamic modal operators that can change the frame of the model during the evaluation of a formula. In particular, we extend the basic modal language with modalities that are able to swap, delete or add pairs of related elements of the domain, while traversing an edge of the accessibility relation. We study these languages together with the sabotage modal logic, which can arbitrarily delete edges of the model.

We show that the complexity of their model checking problems is PSpace-complete. We also consider versions of the model checking problems where the model is fixed (formula complexity), and when the formula is fixed (program complexity).