Moshe Y. Vardi
Rive University
May 14, 2008
Title: From Philosophical to Industrial Logics
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
industrial model-checking tools. This talk attempts to trace
the tangled threads of this development.