Brigitte Vallée to be awarded the Légion d’Honneur on the 20 of January 2016. The act will take place just after the
Journées nationales 2016 of the GDR Informatique Mathématique. Please consult here for more details.Brigitte Vallée to be awarded the Légion d’Honneur on the 20 of January 2016. The act will take place just after the
Journées nationales 2016 of the GDR Informatique Mathématique. Please consult here for more details.Brigitte Vallée to be awarded the Légion d’Honneur on the 20 of January 2016. The act will take place just after the
Journées nationales 2016 of the GDR Informatique Mathématique. Please consult here for more details.

From 17 November to 1 December Professor Frédérique Bassino from the Laboratoire d’Informatique de
Paris-Nord (http://lipn.univ-paris13.fr/~bassino/) will visit the Depto. de Computación of the FCEyN (UBA).
She will be offering an 8 hour course on her area of expertise, namely Analytic Combinatorics.
Below is the course syllabus  (4 classes of 2 hours each;  in English).

Nombre del curso:  Introducción a la Combinatoria Analítica

Este curso es una introducción a la combinatoria analítica, una rama de
la matemática relativamente reciente, basada en combinatoria y técnicas
de análisis y que ha resultado de utilidad para estudiar propiedades de
(grandes) estructuras combinatorias discretas .
El curso se enfocará en dos herramientas fundamentales y
representativas: el método simbólico (técnicas combinatorias) y el
análisis de singularidades (técnicas analíticas).
Las funciones generatrices funcionan como puente entre estos dos
métodos: en el primer caso se estudian desde un punto de vista formal y
en el segundo se ven como funciones analíticas.
Discutiremos brevemente otras técnicas importantes, métodos y
herramientas tales como el método del punto de silla. Ilustraremos con
varios ejemplos las bases de la Combinatoria Analítica con aplicaciones
a Ciencias de la Computación, y más específicamente al análisis de
algoritmos y estructuras de datos.
Se requieren algunos conocimientos de algoritmos, probabilidades
elementales, y es de utilidad aunque no indispensable tener
conocimientos de combinatoria y análisis complejo.

Bibliografía: Ph. Flajolet and R. Sedgewick “Analytic Combinatorics”,
Cambridge University Press (2009) available for free on the web
http://algo.inria.fr/flajolet/Publications/book.pdfFrom 17 November to 1 December Professor Frédérique Bassino from the Laboratoire d’Informatique de
Paris-Nord (http://lipn.univ-paris13.fr/~bassino/) will visit the Depto. de Computación of the FCEyN (UBA).
She will be offering an 8 hour course on her area of expertise, namely Analytic Combinatorics.
Below is the course syllabus  (4 classes of 2 hours each;  in English).

Nombre del curso:  Introducción a la Combinatoria Analítica

Este curso es una introducción a la combinatoria analítica, una rama de
la matemática relativamente reciente, basada en combinatoria y técnicas
de análisis y que ha resultado de utilidad para estudiar propiedades de
(grandes) estructuras combinatorias discretas .
El curso se enfocará en dos herramientas fundamentales y
representativas: el método simbólico (técnicas combinatorias) y el
análisis de singularidades (técnicas analíticas).
Las funciones generatrices funcionan como puente entre estos dos
métodos: en el primer caso se estudian desde un punto de vista formal y
en el segundo se ven como funciones analíticas.
Discutiremos brevemente otras técnicas importantes, métodos y
herramientas tales como el método del punto de silla. Ilustraremos con
varios ejemplos las bases de la Combinatoria Analítica con aplicaciones
a Ciencias de la Computación, y más específicamente al análisis de
algoritmos y estructuras de datos.
Se requieren algunos conocimientos de algoritmos, probabilidades
elementales, y es de utilidad aunque no indispensable tener
conocimientos de combinatoria y análisis complejo.

Bibliografía: Ph. Flajolet and R. Sedgewick “Analytic Combinatorics”,
Cambridge University Press (2009) available for free on the web
http://algo.inria.fr/flajolet/Publications/book.pdfEntre el 17 de Noviembre y el 1 de Diciembre la Profesora Frederique Bassino del Laboratoire d’Informatique de
Paris-Nord (http://lipn.univ-paris13.fr/~bassino/) visitará el Depto. de Computación de la FCEyN (UBA).
Ella ofreció dictar un curso introductorio de 8hs en el tema de su especialidad, Combinatoria Analítica.
Se anexa el programa (4 clases de 2hs;  en Inglés).

Nombre del curso:  Introducción a la Combinatoria Analítica

Este curso es una introducción a la combinatoria analítica, una rama de
la matemática relativamente reciente, basada en combinatoria y técnicas
de análisis y que ha resultado de utilidad para estudiar propiedades de
(grandes) estructuras combinatorias discretas .
El curso se enfocará en dos herramientas fundamentales y
representativas: el método simbólico (técnicas combinatorias) y el
análisis de singularidades (técnicas analíticas).
Las funciones generatrices funcionan como puente entre estos dos
métodos: en el primer caso se estudian desde un punto de vista formal y
en el segundo se ven como funciones analíticas.
Discutiremos brevemente otras técnicas importantes, métodos y
herramientas tales como el método del punto de silla. Ilustraremos con
varios ejemplos las bases de la Combinatoria Analítica con aplicaciones
a Ciencias de la Computación, y más específicamente al análisis de
algoritmos y estructuras de datos.
Se requieren algunos conocimientos de algoritmos, probabilidades
elementales, y es de utilidad aunque no indispensable tener
conocimientos de combinatoria y análisis complejo.

Bibliografía: Ph. Flajolet and R. Sedgewick “Analytic Combinatorics”,
Cambridge University Press (2009) available for free on the web
http://algo.inria.fr/flajolet/Publications/book.pdf

Pablo Barenbaum, PhD student at UBA, visits the University Paris Diderot from 13 October to 14 November 2015. He will be collaborating with Delia Kesner (U. Paris Diderot) and Beniamino Accattoli (INRIA).Pablo Barenbaum, PhD student at UBA, visits the University Paris Diderot from 13 October to 14 November 2015. He will be collaborating with Delia Kesner (U. Paris Diderot) and Beniamino Accattoli (INRIA).Pablo Barenbaum, PhD student at UBA, visits the University Paris Diderot from 13 October to 14 November 2015. He will be collaborating with Delia Kesner (U. Paris Diderot) and Beniamino Accattoli (INRIA).

Nicolás Álvarez will visit the Université Paris-Diderot from 19 October  to 13 November 2015. He will collaborate with Prof.  Olivier Carton.Nicolás Álvarez will visit the Université Paris-Diderot from 19 October  to 13 November 2015. He will collaborate with Prof.  Olivier Carton.Nicolás Álvarez will visit the Université Paris-Diderot from 19 October  to 13 November 2015. He will collaborate with Prof.  Olivier Carton.

Brigitte Vallée and Valérie Berthé will visit Buenos Aires in October 2015, more precisely from the 14 to the 19 of October. They will collaborate with Eda Cesaratto at the Universidad Nacional de General Sarmiento.

Brigitte Vallée y Valérie Berthé will visit Buenos Aires in October 2015, more precisely from the 14 to the 19 of October. They will collaborate with Eda Cesaratto at the Universidad Nacional de General Sarmiento.

Brigitte Vallée y Valérie Berthé will visit Buenos Aires in October 2015, more precisely from the 14 to the 19 of October. They will collaborate with Eda Cesaratto at the Universidad Nacional de General Sarmiento.

Diego Figueira (UBA and CONICET) will visit LaBRI (Laboratoire Bordelais de Recherche en Informatique, Bordeaux) from the 1st to the 16th of September. Sergio Abriola (PhD student at UBA and CONICET) will be visiting the same laboratory from 1 of September to the 2 of October. Both are collaborating with Diego Figueira in topics related to “data-aware logics”.

Diego Figueira (UBA and CONICET) will visit LaBRI (Laboratoire Bordelais de Recherche en Informatique, Bordeaux) from the 1st to the 16th of September. Sergio Abriola (PhD student at UBA and CONICET) will be visiting the same laboratory from 1 of September to the 2 of October. Both are collaborating with Diego Figueira in topics related to “data-aware logics”.

Diego Figueira (UBA and CONICET) will visit LaBRI (Laboratoire Bordelais de Recherche en Informatique, Bordeaux) from the 1st to the 16th of September. Sergio Abriola (PhD student at UBA and CONICET) will be visiting the same laboratory from 1 of September to the 2 of October. Both are collaborating with Diego Figueira in topics related to “data-aware logics”.

Thibaut Balabonski (Maître de conférences à l’Université Paris Sud, LRI, équipe VALS) visited UBA and UNQ in the setting of an ECOS Sud collaboration project. He participated in discussions with Pablo Barenbaum and Eduardo Bonelli. He also gave a talk at the LIA Workshop. Follow the links for further details.

 Thibaut Balabonski (Maître de conférences à l’Université Paris Sud, LRI, équipe VALS) visited UBA and UNQ in the setting of an ECOS Sud collaboration project. He participated in discussions with Pablo Barenbaum and Eduardo Bonelli. He also gave a talk at the LIA Workshop. Follow the links for further details.Thibaut Balabonski (Maître de conférences à l’Université Paris Sud, LRI, équipe VALS) visited UBA and UNQ in the setting of an ECOS Sud collaboration project. He participated in discussions with Pablo Barenbaum and Eduardo Bonelli. He also gave a talk at the LIA Workshop. Follow the links for further details.

Frédéric PROST (Associate Professor at LIG , in the CAPP team) and Martin Monperrus (Associate professor at the University of Lille (France) and a member of INRIA’s SPIRALS research group) recently visited the Departamento de Computación (FCEyN, UBA) and gave courses at the winter school in Computer Science ECI 2015. Follow the links for further information.

Frédéric PROST (Associate Professor at LIG , in the CAPP team) and Martin Monperrus (Associate professor at the University of Lille (France) and a member of INRIA’s SPIRALS research group) recently visited the Departamento de Computación (FCEyN, UBA) and gave courses at the winter school in Computer Science ECI 2015. Follow the links for further information.

Frédéric PROST (Associate Professor at LIG , in the CAPP team) and Martin Monperrus (Associate professor at the University of Lille (France) and a member of INRIA’s SPIRALS research group) recently visited the Departamento de Computación (FCEyN, UBA) and gave courses at the winter school in Computer Science ECI 2015. Follow the links for further information.

The workshop will be held at the Departamento de Computación of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!

10:00-10:15 Sergio Yovine and Eduardo Bonelli
Opening remarks

10:15-10:50 Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

10:50-11:25 Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

11:25-11:40 Coffee break

11:40-12:15 Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

12:15-12:50 Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

12:50-14:00 Lunch

14:00-14:35 Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

14:35-15:10 Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

15:10-15:25 Coffee break

15:25-16:00 Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

16:00-16:15 Sergio Yovine and Eduardo Bonelli
Closing remarks

————————————————————————————————————–
Abstracts of talks:

Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.

Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time. While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4).
Joint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong

Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.

Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

Proof assistants like Coq are now eminently effective for formalizing “research-grade” mathematics, verifying serious software systems, and, more broadly, enabling researchers to mechanize and breed confidence in their results. Nevertheless, the mechanization of substantial proofs typically requires a significant amount of manual effort. To alleviate this burden, proof assistants typically provide an additional language for tactic programming. Tactics support general-purpose scripting of automation routines, as well as fine control over the state of an interactive proof. However, for most existing tactic languages (e.g., ML, Ltac), the price to pay for this freedom is that the behavior of a tactic lacks any static specification within the base logic of the theorem prover (such as, in Coq, a type). As a result of being untyped, tactics are known to be difficult to compose, debug, and maintain.

In my thesis I developed two different approaches to typed tactic programming in the context of Coq: Lemma Overloading and Mtac. Both approaches rely heavily on the unification algorithm of Coq, which is a complex mixture of different heuristics and has not been formally specified. Therefore, I also build and describe a new unification algorithm better suited for tactic programming in Coq. In this talk I describe the high level achievements of my work and introduce in depth Mtac, a new programming language for typed tactic programming in Coq.

Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\mathcal K}(\alpha)$ of the fractional parts of the multiples of a real $\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\mathcal K}(\alpha)$, and is useful to study the pseudo-randomness of the sequence ${\mathcal K}(\alpha)$ for a random input $\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\alpha$ is a random real, and the case when $\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\alpha$ plays an important rôle. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\infty$ and the unconstrained case $M = \infty$. Joint work with Brigitte Vallée, CNRS and Université de Caen, France.

Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler). This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.

Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.

The workshop will be held at the Departamento de Computación of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!

10:00-10:15 Sergio Yovine and Eduardo Bonelli
Opening remarks

10:15-10:50 Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

10:50-11:25 Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

11:25-11:40 Coffee break

11:40-12:15 Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

12:15-12:50 Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

12:50-14:00 Lunch

14:00-14:35 Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

14:35-15:10 Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

15:10-15:25 Coffee break

15:25-16:00 Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

16:00-16:15 Sergio Yovine and Eduardo Bonelli
Closing remarks

————————————————————————————————————–
Abstracts of talks:

Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.

Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time. While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4).
Joint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong

Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.

Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

Proof assistants like Coq are now eminently effective for formalizing “research-grade” mathematics, verifying serious software systems, and, more broadly, enabling researchers to mechanize and breed confidence in their results. Nevertheless, the mechanization of substantial proofs typically requires a significant amount of manual effort. To alleviate this burden, proof assistants typically provide an additional language for tactic programming. Tactics support general-purpose scripting of automation routines, as well as fine control over the state of an interactive proof. However, for most existing tactic languages (e.g., ML, Ltac), the price to pay for this freedom is that the behavior of a tactic lacks any static specification within the base logic of the theorem prover (such as, in Coq, a type). As a result of being untyped, tactics are known to be difficult to compose, debug, and maintain.

In my thesis I developed two different approaches to typed tactic programming in the context of Coq: Lemma Overloading and Mtac. Both approaches rely heavily on the unification algorithm of Coq, which is a complex mixture of different heuristics and has not been formally specified. Therefore, I also build and describe a new unification algorithm better suited for tactic programming in Coq. In this talk I describe the high level achievements of my work and introduce in depth Mtac, a new programming language for typed tactic programming in Coq.

Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\mathcal K}(\alpha)$ of the fractional parts of the multiples of a real $\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\mathcal K}(\alpha)$, and is useful to study the pseudo-randomness of the sequence ${\mathcal K}(\alpha)$ for a random input $\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\alpha$ is a random real, and the case when $\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\alpha$ plays an important rôle. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\infty$ and the unconstrained case $M = \infty$. Joint work with Brigitte Vallée, CNRS and Université de Caen, France.

Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler). This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.

Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.

The workshop will be held at the Departamento de Computación of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!

10:00-10:15 Sergio Yovine and Eduardo Bonelli
Opening remarks

10:15-10:50 Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

10:50-11:25 Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

11:25-11:40 Coffee break

11:40-12:15 Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

12:15-12:50 Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

12:50-14:00 Lunch

14:00-14:35 Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

14:35-15:10 Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

15:10-15:25 Coffee break

15:25-16:00 Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

16:00-16:15 Sergio Yovine and Eduardo Bonelli
Closing remarks

————————————————————————————————————–
Abstracts of talks:

Diego Figueira (CNRS,LaBRI, France)
Logics for words and trees with data

The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.

Flavia Bonomo (UBA,CONICET)
Three-colouring graphs without triangles or induced paths on seven vertices

We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time. While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4).
Joint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong

Alejandro Díaz-Caro (UNQ)
Projective quantum measurement in the lambda calculus

By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.

Beta Ziliani (FAMAF, CONICET)
Interactive Typed Tactic Programming in the Coq Proof Assistant

Proof assistants like Coq are now eminently effective for formalizing “research-grade” mathematics, verifying serious software systems, and, more broadly, enabling researchers to mechanize and breed confidence in their results. Nevertheless, the mechanization of substantial proofs typically requires a significant amount of manual effort. To alleviate this burden, proof assistants typically provide an additional language for tactic programming. Tactics support general-purpose scripting of automation routines, as well as fine control over the state of an interactive proof. However, for most existing tactic languages (e.g., ML, Ltac), the price to pay for this freedom is that the behavior of a tactic lacks any static specification within the base logic of the theorem prover (such as, in Coq, a type). As a result of being untyped, tactics are known to be difficult to compose, debug, and maintain.

In my thesis I developed two different approaches to typed tactic programming in the context of Coq: Lemma Overloading and Mtac. Both approaches rely heavily on the unification algorithm of Coq, which is a complex mixture of different heuristics and has not been formally specified. Therefore, I also build and describe a new unification algorithm better suited for tactic programming in Coq. In this talk I describe the high level achievements of my work and introduce in depth Mtac, a new programming language for typed tactic programming in Coq.

Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)
Metrical versions of the Two Distances Theorem

We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\mathcal K}(\alpha)$ of the fractional parts of the multiples of a real $\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\mathcal K}(\alpha)$, and is useful to study the pseudo-randomness of the sequence ${\mathcal K}(\alpha)$ for a random input $\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\alpha$ is a random real, and the case when $\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\alpha$ plays an important rôle. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\infty$ and the unconstrained case $M = \infty$. Joint work with Brigitte Vallée, CNRS and Université de Caen, France.

Thibaut Balabonski (INRIA, U. Paris Sud)
Low-level C code optimisations: are they valid?

Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler). This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.

Juan Pablo Galleoti (UBA, CONICET)
Towards An Evolutionary Approach to Unit-Level Invariant Discovery

Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.