Амир Пнуэли родился 22 апреля 1941 года. Известен как американский и израильский учёный в области теории вычислительных систем.
Биография
Амир Пнуэли родился в Нахалале (Палестина, сейчас Израиль).
Обучался в Израильском технологическом институте (Хайфа), в котором получил степень бакалавра. Обучаясь в Институте Вейцмана Амир Пнуэли в 1967 году защищает докторскую диссертацию и получает степень доктора философии по прикладной математике.
Работает в Стэнфордском университете в качестве постдока. Затем возвращается в Реховот, а в 1973 году переезжает в Тель-Авив, где основывает факультет информатики в Тель-Авивском университете и становится его первым деканом.
С 1981 года переходит на должность профессора информатики в Институт Вейцмана.
В 1999 году начинает работать на должности профессора в Нью-Йоркском университете.
В 2007 году Амира Пнуэли избирают действительным членом АВТ (Ассоциации вычислительной техники).
Амир Пнуэли является основателем двух фирм – AdCad и Mini-Systems.
Является автором около 30 научных работ.
Амир Пнуэли умер от кровоизлияния в мозг в возрасте 68 лет 2 ноября 2009 года в Нью-Йорке (США).
Научные интересы
Семантика и верификации параллельных программ, временная логика, логика программ, спецификации и непроцедурные языки, автоматические методы доказательства правильности, контроля и синтеза программ, теория вычислений, теория схем и ее отношения к формальной теории языков, технические требования, контроль и систематическое развитие реального времени и гибридных систем. Доработка с использованием темпоральной логики. Композиционное проверка реактивных, в режиме реального времени, и гибридных систем. Синтез таких систем.
Научно-исследовательская работа
Профессор Пнуэли известен введением временной логики в область компьютерных наук, его работой по применению временной логики и подобных формализмов для спецификации и верификации реактивных систем, определением класса «реактивных систем», развитием богатой и подробной методики, основанной на временной логике, для формальной обработки реактивной системы; расширяя эту методологию в области систем реального времени.
Кроме теоретической работы, связанной с полной системой аксиом и теорией доказательств для верификации программ временной логики, Пнуэли также способствовал алгоритмическим исследованиям в этой области. Он разработал дедуктивную систему линейного времени временной логики и модель проверки алгоритмов для проверки временных свойств конечных систем. Вместе с Дэвидом Харелем, Пнуэли работал над семантикой и реализацией Statecharts, визуальным языком для спецификации, моделирования и прототипирования реактивных систем. Этот язык был применен в авионике, транспорте и электронных аппаратных системах. В настоящее время его научные интересы включают синтез реактивных модулей автоматической проверки многопроцессорных систем, процессов и методов спецификации, которые сочетают переходные системы с временной логикой.
В соавторстве с Зохаром Манной А. Пнуэли является автором ряда учебников по временной логике и ее применению к реактивным системам.
Награды
В 1996 году Пнуэли за выдающийся вклад в верификацию систем и программ и за плодотворную работу по внедрению темпоральной логики в вычислительные науки награжден премией Тьюринга.
В 1997 году получает почётный докторский титул от Уппсальского университета (Швеция).
В следующем году Амир Пнуэли получает почётный докторский титул от Университета Жозефа Фурье (Гренобль, Франция).
В 2000 году А. Пнуэли награжден Государственной премией Израиля.
