I just finished integrating LTL model-checking into ASAP. This is joint work with Sami Evangelista and Thomas Vestergaard. Basically, I've made the translation from LTL to a Büchi automaton, Sami made the nested depth-first checker, and Thomas put it together, added a bunch of utility functions, and made the initial integration into ASAP. After
Time person of the year 2006, Nobel Peace Prize winner 2012.