Ja sitten sellainen pysähtymistesteri olis kanssa kiva

Teräsjumalaprojektien, apurahahakemusten, tutkimuspalaverien, sosiaalisten velvoitteiden ja Islanti-aiheisen seminaarin täyttämä päivä ei erityisesti tue tämänkaltaisia fiktiivisiä kaunokirjallisia projekteja. Tyydyn siis kahteen huomioon.

Ensimmäinen huomio. Antaumuksellisesta akateemisesta prokrastinaatiosta huolimatta erityistutkija kutsuttiin vierailevaksi esiintyjäksi Torontoon, CASCON 2005-workshoppiin, tarkoituksenaan jakaa syvällistä viisautta kuulijoille muiden esiintyjien, kuten herra Czarneckin kanssa. No, ei itkeä saa eikä meluta saa, kun kerran lennot ja majoitus maksetaan järjestävän konttorin puolesta.

Ja kun kerran lähdettiin näille linjoille, voisiko joku viisaampi valistaa minua miksi seuraava luentoaihio tuntuu jotenkin epäilyttävältä:

Speaker: Dr. Byron Cook, Microsoft Research
TITLE: Automatically Proving the Termination of C Programs

In this talk I will discuss Terminator, the first known automatic program termination prover to support large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers.

Terminator is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. Additionally, to increase the proof power, Terminator computes inductive invariants of the program when checking the lemmas that imply termination. The talk will close with results from recent experiments with Terminator on dispatch routines from Windows device drivers.

Kiitoksia. Keskiolut loppuu, siirryn seuraamaan henkilökohtaisen kinon tämänöistä tarjontaa.