Intel
Профессор Харрисон занимается формальной верификацией в компании Intel Corporation. Его основной специализацией является верификация алгоритмов, работающих с числами с плавающей точкой. Профессор Харрисон внёс вклад в разработку стандарта IEEE 754.
Является автором книги Handbook of Practical Logic and Automated Reasoning
, а также членом редколлегии журнала Journal of Automated Reasoning.
Личная страница: http://www.cl.cam.ac.uk/~jrh13/
Курс | Семестр |
---|---|
Автоматическое доказательство теорем | осень 2013 |