<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">DEPARTMENT OF COMPUTER SCIENCE<div><br class="webkit-block-placeholder"></div><div>UNIVERSITY OF CHICAGO</div><div><br class="webkit-block-placeholder"></div><div>Date: Monday, April 21, 2008</div><div>Time: 2:30 p.m.</div><div>Place: Ryerson 251, 1100 E. 58th Street</div><div><br class="webkit-block-placeholder"></div><div>----------------------------------------------------------</div><div><br class="webkit-block-placeholder"></div><div>Speaker:<span class="Apple-tab-span" style="white-space: pre; "> </span>Moshe Vardi</div><div><br class="webkit-block-placeholder"></div><div>From:<span class="Apple-tab-span" style="white-space: pre; "> </span>Rice University</div><div><br class="webkit-block-placeholder"></div><div>Web page:<span class="Apple-tab-span" style="white-space: pre; "> </span><span class="Apple-style-span" style="color: rgb(0, 0, 255); "><a href="http://www.cs.rice.edu/~vardi/">http://www.cs.rice.edu/~vardi/</a></span></div><!--StartFragment--><!--StartFragment--><div><br class="webkit-block-placeholder"></div><div>Title: From Philosophical to Industrial Logics</div><div><br class="webkit-block-placeholder"></div><div>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.</div><!--StartFragment--></body></html>