Séminaire, 9 avril 2015
Programme
 10:30 – 12:00

Igor Walukiewicz (CNRS, Labri)
Our objective is to verify behavioural properties of programs, as for example "an open stream is eventually closed", or "a login function is called infinitely often". We use lambda Ycalculus, the simply typed lambdacalculus with the fixpoint combinator, as an intermediate language. The approach we pursue consists of two steps: translate a program into a term of lambda Ycalculus, and then analyse the Bohm tree of the resulting term. Thanks to the result of Ong it is decidable if the Bohm tree of a given term satisfies a given property expressed in monadic secondorder logic; this is a classical logic for tree properties that is capable to express many interesting properties of computations. We solve the verification problem by a mix of automata and semantic techniques, in particular we construct appropriate models of lambda Y calculus.
The talk will start with the introduction to the verification problem for higherorder programs. Most type systems for programming languages concentrate on, some, safety properties of programs. We will present monadic secondorder logic (MSOL) on binary trees, and give indications why verification of MSOL properties is more complex than just for safety properties. Next, we will adapt the notion of recognizability, the classical notion from language theory, to our setting. We will state our main result saying that for every MSOL property there is a finitary model of the lambda Ycalculus recognizing this property. Finally, we will discuss some corollaries of this theorem concerning verification of programs as well as program transformation, and program synthesis.
This is joint work with Sylvain Salvati.
 14:00 – 15:00

Charles Grellois (Univ. Paris Diderot)
To modelcheck a higherorder functional program with recursion, one can abstract it as a lambda Yterm normalizing to a tree over a signature of actions, which approximates the set of behaviours of this program. Running an alternating parity automaton over this tree is then a way to ensure that it respects a given MSO specification.
A connection between higherorder modelchecking and linear logic appears naturally when one considers the linear typing of lambdaterms. Interpreted in the relational model of linear logic, the duals of these types correspond precisely to the set of alternating automata (without parity condition), leading to a semantic modelchecking approach: lambdaterms generating trees and alternating tree automata are given dual semantics in the relational model, so that their interaction computes the set of states from which an automaton accepts the tree computed by a term. The modelchecking problem may then be solved by checking that the initial state of the automaton belongs to the result.
In this talk, we explain how this theorem can be generalized to lambdaterms with recursion, and to alternating automata with a parity condition. This requires us to consider an infinitary variant of the relational semantics of linear logic, and to define a coloured exponential modality over it. We finally devise a fixed point operator verifying directly at the level of denotations the parity condition of alternating parity tree automata, and obtain the desired generalized semantic modelchecking theorem.
We finally recast our approach in a finitary model of linear logic, provided by its Scott semantics, and explain how it leads to a decidability proof of the higherorder modelchecking problem.
(joint work with PaulAndré Melliès)
 15:30 – 16:30

Sylvain Salvati (INRIA, Université de Bordeaux)Invited talk: Model construction for higherorder modelchecking
When dealing with finite state properties, it is usual to have some finite algebraic structures (e.g. finite monoids in the case of finite state automata on strings) that represent those properties. When dealing with logical properties of programs that are computed by finite state automaton, the question of what is an "adequate" finite algebraic structure arises. Having such a structure would entail a sort of modularity in program verification, but it also gives some strong understanding of how the properties can be checked.
In the context of higherorder verification, programs are models as lambdaterms and it is natural to think about denotational domains as a possible candidate. Finitary Scott domains only capture very simple properties of the Bohm trees generated by higherorder programs. This talk will illustrate how to enrich Scott domains so that they can capture wider classes of finite state properties.
(joint work with Igor Walukiewicz)