Prof. Moshe Y. Vardi,
Department of Computer Science,
Rice University, Houston,
From Philosophical to
18 dicembre 2007, ore 11:00
Dipartimento di Informatica e Sistemistica "Antonio Ruberti"
SAPIENZA Università di Roma,
via Ariosto 25, Roma,
(il seminario si svolgerà presso l'Aula Magna)
ABSTRACT: One of the surprising developments in the area of program verification is how several ideas introduced
by logicians in the first part of the 20th century ended up yielding at the start of the 21st century industry-standard
property-specification languages called PSL and SVA. This development was enabled by the equally unlikely transformation
of the mathematical machinery of automata on infinite words, introduced in the early 1960s for second-order arithmetics,
into effective algorithms for model-checking tools. This talk attempts to trace the tangled threads of this development.