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 Y-calculus, the simply typed lambda-calculus with the fixpoint combinator, as an intermediate language. The approach we pursue consists of two steps: translate a program into a term of lambda Y-calculus, 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 second-order 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 higher-order programs. Most type systems for programming languages concentrate on, some, safety properties of programs. We will present monadic second-order 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 Y-calculus 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 model-check a higher-order functional program with recursion, one can abstract it as a lambda Y-term 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 higher-order model-checking and linear logic appears naturally when one considers the linear typing of lambda-terms. 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 model-checking approach: lambda-terms 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 model-checking 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 lambda-terms 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 model-checking 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 higher-order model-checking problem.
(joint work with Paul-André Melliès)
- 15:30 – 16:30
-
Sylvain Salvati (INRIA, Université de Bordeaux)Invited talk: Model construction for higher-order model-checking
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 higher-order verification, programs are models as lambda-terms 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 higher-order 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)
