Evènement pour le groupe Séminaire Méthodes Formelles


Date 2017-03-07  11:00-12:00
TitreVerifying properties of functional programs: from the deterministic to the probabilistic case 
RésuméIn functional programs, also called higher-order programs, functions may take functions themselves as arguments. As a result, their model-checking relies in most approaches on semantic or type-theoretic tools. In this talk, I will explain how an analysis based on linear logic of a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for model-checking. This model is such that, when interpreting a term with recursion representing the tree of traces of a functional program, its denotation determines whether it satisfies a MSO property of interest. A related and similar model was obtained independently by Salvati and Walukiewicz. In the second part of the talk, I will discuss the verification of termination for functional programs with recursion and probabilistic choice. Dal Lago and I defined recently a type system which is such that typable programs terminate with probability 1. In other terms, their set of diverging executions is negligible. If time allows, I will sketch ideas towards an extension of the model-checking results of the deterministic case to quantitative logics and functional programs with recursion. 
Lieu178 
OrateurCharles Grellois 
Emailhttp://research.grellois.fr/ 
UrlUniversity of Bologna 



Aucun document lié à cet événement.

Retour
Retour à l'index