13 March 2012
Cachan, France
Colloquium on Theory of Software Verification
March 13, 2012 - LSV - Cachan
http://www.lsv.ens-cachan.fr/Events/ctsv/
A special event with two talks, followed by the Habilitation defense
of Laurent Doyen. The confirmed invited speakers are:
* Prof. Rupak Majumdar, MPI Kaiserslautern & UCLA
* Prof. Moshe Y. Vardi, Rice University
PROGRAMME
Tuesday, March 13th, 2012
10:00 Moshe Vardi, The Rise and Fall of Linear Temporal Logic
11:30 Rupak Majumdar, TBA
14:30 Laurent Doyen, Games and Automata: From Boolean to Quantitative
Verification
REGISTRATION
The event is open to the public and free. For organizational purposes,
please let us know if you plan to attend one of the two morning talks,
you can register at http://www.lsv.ens-cachan.fr/Events/ctsv/register
A confirmation will be sent to you by e-mail.
LOCATION
The talks will take place on the campus of ENS Cachan (Ecole normale
superieure de Cachan). Travel instructions are available at:
http://www.lsv.ens-cachan.fr/Events/ctsv/
CONTACT
This event is organized by Laurent Doyen and Alain Finkel.
See http://www.lsv.ens-cachan.fr/Events/ctsv/ for up-to-date information.
ABSTRACTS OF THE TALKS
Moshe Y. Vardi (Rice University, USA)
=====================================
The Rise and Fall of Linear Temporal Logic
One of the surprising developments in the area of program verification
in the late part of the 20th Century is the emergence of Linear Temporal
Logic (LTL), a logic that emerged in philisophical studies of free will,
as the cannonical language for describing temporal behavior of computer
systems. LTL, however, is not expressive enough for industrial applications.
The first decade of the 21 Century saw the emergence of
industrial temporal logics such as ForSpec, PSL, and SVA. These logics,
however, are not clean enough to serve as objects of theoretical study.
This talk will describe the rise and fall of LTL, and will propose a new
cannonical temporal logic: Linear Dynamic Logic (LDL).
Rupak Majumdar (MPI, Germany & UCLA, USA)
=========================================
TBA
Laurent Doyen (LSV, ENS Cachan & CNRS, France)
==============================================
Habilitation Thesis
Games and Automata: From Boolean to Quantitative Verification
Abstract. This talk presents a selection of results in the traditional
verification of finite-state games and automata (new efficient
algorithms for decision problems in games and automata theory), then
presents extensions of the traditional models to quantitative games and
automata, and new results in complexity, algorithmics, and expressive
power of the new models.
http://www.lsv.ens-cachan.fr/Events/ctsv/
k