Links' Seminars and Public Events | ![]() ![]() |
Fri, March 18, 2016 all day | Visit of Charles Paperman, Université Paris 7 Inria Lille |
Fri, March 11, 2016 10:30 am 12:00 pm | Seminar Links by Sylvain Salvati: Behavioral verification of higher-order programs Abstract: Higher-order constructions make their way into main stream programming languages like Java, C++, python, rust... These constructions bring new challenges to the verification of programs as they make their control flow more complex. In this talk, I will present how methods coming from denotational semantics can prove decidable the verification of certain properties of higher-order programs. These properties are expressed by means of finite state automata of the possibly infinite execution trees generated by the programs and can capture safety properties but also liveness and fairness properties. |
Fri, March 11, 2016 all day | Sylvain Salvati: visit and Talk |
Wed, March 9, 2016 1:30 pm 2:00 pm | cristan duriez 30 minutes de science inria lille |
Fri, March 4, 2016 all day | Colis ANR project: general meeting Inria Lille, Salle B21 |
Thu, March 3, 2016 all day | Kim Nguyen: visit for discussion with Links' members (no talk) Université Paris Sud www.lri.fr/~kn/ B218 |
Fri, February 19, 2016 11:00 am 3:00 pm | CNRS, Université Lens |
Thu, January 21, 2016 11:00 am 1:00 pm | Seminar by Vincent Penelle: "Rewriting high-order stack trees" Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the satisfaction of any formula written in monadic second order logic (respectively first order logic with reachability predicates) can be decided on such a graph. The purpose of this talk is to propose a common extension to both higher-order stack operations and ground tree rewriting. We introduce a model of higher-order ground tree rewriting over trees labelled by higher-order stacks (henceforth called stack trees), which syntactically coincides with ordinary ground tree rewriting at order 1 and with the dynamics of higher-order pushdown automata over unary trees. The infinite graphs generated by this class have a decidable first order logic with reachability. Formally, an order n stack tree is a tree labelled by order n-1 stacks. Operations of ground stack tree rewriting are represented by a certain class of connected DAGs labelled by a set of basic operations over stack trees describing of the relative application positions of the basic operations appearing on it. Applying a DAG to a stack tree t intuitively amounts to paste its input vertices to some leaves of t and to simplify the obtained structure, applying the basic operations labelling the edges of the DAG to the leaves they are appended to, until either a new stack tree is obtained or the process fails, in which case the application of the DAG to t at the chosen position is deemed impossible. This model is a common extension to those of higher-order stack operations presented by Carayol and of ground tree transducers presented by Dauchet and Tison. As further results we can define a notion of recognisable sets of operations through a generalisation. The proof that the graphs generated by a ground stack tree rewriting system have a decidable first order theory with reachability is inspired by the technique of finite set interpretations presented by Colcombet and Loding. "Lille-Salle B21" |
Thu, January 14, 2016 all day | visite pierre senellart |
Tue, January 12, 2016 to Thu, January 14, 2016 all day | visite Antoine Amarilli |