Orateur : Charles Grellois (LIS)
Titre : When type theory meets model-checking
Résumé : Type theory and model-checking are two formal methods, aiming at ensuring the correctness of programs. In type theory, the idea is to annotate the instructions of the program with the properties they satisfy, so as to statically control how they will evolve during the computation, and to conclude that the program is correct — or not. In model-checking, one typically abstracts the program as a mathematical model, as a graph for instance, representing an approximation of its behavior. Then, an appropriate logical formula is devised over this program, and an algorithm checks automatically whether the abstract model satisfies the requirement. In the analysis of functional programs, higher-order constructions are possible: one can define functions that themselves take functions as inputs. Type theory is particularly useful to analyze such situations, as I will explain during the talk. I will first give a brief idea of what model-checking is, then explain what are the basics of type theory, and in a third time show how they where combined by Kobayashi in 2009 to perform model-checking of functional programs. If time allows, I will spend the last minutes giving an overview of the research I did in the last years building up on Kobayashi’s work and its extension by Kobayashi and Ong.
Orateur : Maximiliano Cristia (U. N. Rosario)
Titre : Programs as formulas (not as proofs)
Résumé : After the Curry-Howard correspondence and the type theories developed in the past decades, it emerged the idea of programs as proofs (of their properties). That is, if we have a proof P of a theorem T, we can make P a program whose type is T. This theory was a major breakthrough in programming language design and software verification. However, in this talk, I’ll show you an alternative and, in some sense, previous view: programs as formulas. In other words, let’s make the very formula to be a program; that is, we don’t need to make a proof to have a program. In particular I’m going to show {log} (setlog), which is a programming language but also an automated theorem prover. In {log} formulas are programs, and programs are formulas. We can use the same tool and the same language to specify programs, to simulate these specifications, to generate test cases and to prove properties of them. {log} works with formulas over the theory of finite sets, which allows for the specification of large classes of programs.
Orateur : Stephane Demri (LSV)
Titre : On The Complexity of Resource-Bounded Logics
Résumé : We characterise the complexity of model-checking problems for resource-bounded logics by taking advantage of recent results on decision problems for alternating VASS. For instance, we show that the model-checking problem for the logic RBATL is 2EXPTIME-complete and we establish that for RBATL* the problem remains decidable. A parameterised version of the logics is also discussed. This is a joint work with Natasha Alechina, Nils Bulling and Brian Logan.