Страна: Израиль

Образование: Доктор философии в области прикладной математики, Научно-исследовательский институт им. Вейцмана, 1967

О лауреате

В 1962 году, во время своего обучения, Pnueli представилась возможность работать на первом в Израиле компьютере WEIZAC – с этого началась его любовь к компьютерам. В 1967 и 1968 годах, после получения степени доктора философии за диссертацию «Calculation of Tides in the Ocean», он работал в Стэнфордском Университете и исследовательском центре IBM, где начал плодотворно сотрудничать с Z. Manna в новой тогда сфере, известной как формальные методы. Его первая работа исследовала формализацию рекурсивных функций и функциональных программ. Во время праздника в Университете Пенсильвании он познакомился с работой философа A. Prior, который разработал «временную логику» для оценки высказываний, чья правдивость меняется со временем. Pnueli первым осознал потенциальную пользу применения работы Prior в компьютерных программах. В то время проверка программ была сосредоточена на программах, которые получают входные данные в начале вычислений и производят вывод в конце («трансформационные»), а основные методы исследований рассматривали все возможные пары состояний программы. Pnueli ввёл концепцию рассуждений о программах как о путях исполнения, которая вдохнула новую жизнь в область верификации программ. В своей оригинальной работе Pnueli рассматривает верификацию программ (позже называемых «реактивными»), которые взаимодействуют с их окружающей средой и не обязательно заканчиваются, например, параллельные вычисления или операционные системы.

Ключевые слова: Temporal logic, Verification, Model checking

Краткая библиография

1.	Pnueli, A., “The Temporal Logic of Programs,” Proceedings of the 18th annual symposium on Foundations of Computer Science, pp. 46-57, 1977. Эта статья произвела революцию в анализе компьютерных программ. Линейная темпоральная логика предлагалась, как единый подход для описаний трансформационных и рекативных систем. Также в статье описана алгоритм проверки моделей программ с конечным числом состояний.
2.	Ben-Ari, M., A. Pnueli and Z. Manna, “The Temporal Logic of Branching Time,” Acta Informatica, Vol. 20, Num. 3, pp. 207-226, 1983 В этой статье представлена ветвящаяся темпоральная логика, предоставляющая первый практичный алгоритм проверки моделей на логику и простую аксиомизацию.
3.	Pnueli,A., “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A survey of Current Trends,” in “Current Trends in Concurrency,” Lecture Notes in Computer Science, Vol. 224, pp. 510-584, 1986. В работе представлен обзор исследований Pnueli и его коллег по применению темпоральной логики для спецификации и верификации реактивных систем и представлены многочисленные примеры.
4.	Pnueli, A., “The Temporal Semantics of Concurrent Programs,” Theoretical Computer Science, Vol. 13, Num. 1, pp. 45-60, 1981. Статья описывает, как найти темпоральную формулу, описывающую систему и получить доказательства, что система удовлетворяет спецификации темпоральной логики.