Seminar on Theory of Software Verification

 [logo.png]

ENS Cachan, March 13th, 2012

A special event with two talks, followed by the Habilitation defense of Laurent Doyen.

The confirmed invited speakers are:

Date and Venue

Tuesday March 13th, 2012.

Venue: Campus of ENS Cachan, Bâtiment d'Alembert, Salle Condorcet.

How to reach the campus by public transportation. A map of Paris subway.
Access map. Campus map.
The room "Salle Condorcet" is on 2nd floor of Bâtiment d'Alembert, see the detailed map.

Programme

Tuesday, March 13th, 2012
09:30 Welcome
10:00 - 11:00 Moshe Y. Vardi
Room: Salle Condorcet		 The Rise and Fall of Linear Temporal Logic
11:00 Coffee break
11:30 - 12:30 Rupak Majumdar
Room: Salle Condorcet		 A Perfect Model for Bounded Verification
12:30 Break
14:30 Laurent Doyen
Room: Salle Condorcet		 Habilitation Thesis - Games and Automata: From Boolean to Quantitative Verification
Closing

Registration

The event is open to the public and free. For organisational purposes, please let us know
if you plan to attend the morning session. Registration is closed

The Habilitation defense in the afternoon is open to the public without registration.


Contact

Please write to the organizers if you have any question.
The organizers are Laurent Doyen, and Alain Finkel.


Abstract of the talks

Moshe Y. Vardi (Rice University, USA)

The Rise and Fall of Linear Temporal Logic

Abstract. 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 Kaiserslautern, Germany & UC Los Angeles, USA)

A Perfect Model for Bounded Verification

Abstract. A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata-theoretic approach to model checking: a system is correct if the language generated by the system is disjoint from the language of bad traces. Regular languages are perfect, but because the disjointness problem for CFLs is undecidable, no class containing the CFLs can be perfect.
    In practice, verification problems for language classes that are not perfect are often under-approximated by checking if the property holds for all behaviors of the system belonging to a fixed subset. A general way to specify a subset of behaviors is by using bounded languages (languages of the form w1* ... wk* for fixed words w1,...,wk). A class of languages C is perfect modulo bounded languages if it is closed under Boolean operations relative to every bounded language, and if the emptiness problem is decidable relative to every bounded language.
    We consider finding perfect classes of languages modulo bounded languages. We show that the class of languages accepted by multi-head pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We show that computations of several known models of systems, such as recursive multi-threaded programs, recursive counter machines, and communicating finite-state machines can be encoded as multi-head pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages.
[Joint work with Javier Esparza and Pierre Ganty]


Laurent Doyen (LSV, ENS Cachan & CNRS, France)

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.

The committee is composed of:
  • Rajeev Alur
  • Ahmed Bouajjani
  • Alain Finkel
  • Jean Goubault-Larrecq
  • Rupak Majumdar
  • Joël Ouaknine
  • Moshe Y. Vardi
  • Igor Walukiewicz

[lsv.png] [logo.png]
Last update: Wed Mar 14 18:23:53 CET 2012.