Сообщение Хосе
Хосе Мессенджер | |
|---|---|
| Рожденный | 1950 (73–74 года) |
| Заголовок | Профессор компьютерных наук |
| Награды |
|
| Академическое образование | |
| Альма-матер | Университет Сарагосы (доктор философии) |
| Диссертация | Примитивная рекурсия в моноидальных категориях [1] (1975) |
| Докторантура | Майкл Пфендер [2] |
| Академическая работа | |
| Дисциплина | Информатика |
| Учреждения | ОИУК |
| Веб-сайт | http://formal.cs.illinois.edu/meseguer/ |
Хосе Месегер Гуайта — испанский учёный-компьютерщик и профессор Университета Иллинойса в Урбане-Шампейне . Он возглавляет университетскую лабораторию формальных методов и декларативных языков.
Карьера
[ редактировать ]Хосе Месегер получил докторскую степень по математике в 1975 году, защитив диссертацию на тему «Примитивная рекурсия в модельных категориях» под руководством Майкла Пфендера в Университете Сарагосы , после чего он работал над докторской диссертацией в Университете Сантьяго-де-Компостела и Калифорнийском университете в Беркли . В 1980 году он присоединился к Лаборатории компьютерных наук в SRI International , в конечном итоге став главным научным сотрудником и главой группы логики и декларативных языков . Он поступил на работу в Университет Иллинойса в 2001 году и в настоящее время является профессором компьютерных наук, где возглавляет лабораторию формальных методов и декларативных языков.
В частности, он работал над разработкой и реализацией декларативных языков, включая OBJ и Maude , а также над переписыванием логики. [3]
Он был награжден Европейской стипендией формальных методов 2019 года . [4] Цитата о награде [5] читает,
Несмотря на все его академические достижения, а также его лидерство и влияние на сообщество формальных методов , мы представляем профессора Хосе Месегера, научного сотрудника FME 2019 года. Профессор Месегер — ведущий исследователь, внесший плодотворный вклад во многие области теоретической информатики и за ее пределы: от общей логики до алгоритмов машинного зрения для роботов . Его работы характеризуются новаторством, концептуальной элегантностью и строгостью в сочетании с практической применимостью.
Профессор Хосе Месегер известен своими плодотворными исследованиями в области алгебраической спецификации , параллелизма , переписывания , логики и компьютерной безопасности . Исследования нашего нового научного сотрудника характеризуются практичной, простой и интуитивно понятной вычислительной логикой и соответствующими методами и инструментами анализа. Результаты исследований были успешно применены к сложным современным системам в различных областях.
Его работа в области компьютерной безопасности особенно значительна. Его формализация невмешательства — одна из самых известных концепций компьютерной безопасности, широко используемая как учеными, так и практиками. Его статья о политиках и моделях безопасности является одной из наиболее цитируемых статей в области компьютерной безопасности (почти 2500 цитирований в Google Scholar ).
Он работал над проектированием и реализацией нескольких декларативных языков, включая OBJ и Maude , над спецификации и проверки формальными методами , над теорией параллелизма , над формальными подходами к объектно-ориентированной спецификации, над параллельным программным обеспечением и архитектурами для декларативных языков, а также над логические основы информатики с использованием эквациональной логики , переписывания логики и теории общей логики.
Он изобретатель переписывания логики и главный разработчик Мод. Его фундаментальным вкладом в формальные методы стало изобретение и развитие переписывания как выразительной и интуитивной вычислительной логики и семантической структуры для параллельных систем. В частности, набор инструментов Maude представляет собой практичный высокопроизводительный инструмент для переписывания.
Важным результатом является демонстрация того, что переписывание логики является естественной и простой моделью параллелизма. Простота и выразительность переписывания логики, реализованная в Моде, привела к спецификации и анализу широкого спектра систем, включая модели вычислений , различную логику, промышленное программирование и языки моделирования .
Он также внес фундаментальный вклад в формальный анализ распределенных систем , объединив рассуждения, основанные на состояниях и действиях, во временной логике ; объединение перезаписи с SMT- решением; и предоставление общих для теории алгоритмов решения SMT, которые можно применять не только к фиксированным заранее определенным теориям, но и к любой теории, удовлетворяющей определенным свойствам. Более поздние исследования включают киберфизические системы , облачные вычисления и биологические системы .
Его научный подход лучше всего описывается изречением «красота – наше дело». Он не боится заходить в области, далекие от того, что мы считаем его зоной комфорта; он на самом деле наслаждается возможностью привнести строгость в другие области и столкнуться с новыми проблемами, которые вдохновляют на новые теоретические разработки.
Свидетельства его друзей и коллег о том, что он старается соблюдать самые высокие этические и научные стандарты в своих исследованиях и в отношениях с коллегами, студентами и другими людьми вокруг него. К новым студентам относятся так же вежливо, как и к ведущим исследователям. Это отражается в том, что многие бывшие студенты продолжают сотрудничать, когда становятся старшими научными сотрудниками.
Он удивительно щедро делится и обсуждает множество идей, исходящих из его богатого ума, и искренне любопытен и ценит другие мнения. Свидетельством этого духа сотрудничества является и то, что в DBLP зарегистрировано 132 соавтора . Несмотря на то, что он является одним из ведущих ученых-компьютерщиков нашего поколения, многие из его сотрудников прежде всего считают его чрезвычайно преданным и настоящим другом.
В 2020 году он был назначен научным сотрудником ACM «за разработку логических методов проектирования и проверки вычислительных систем». [6] [7]
Избранные исследования
[ редактировать ]- Клавель, Мануэль и др. Все о Мод — высокопроизводительной логической структуре: как определять, программировать и проверять системы при переписывании логики. Спрингер-Верлаг, 2007.
- Гоген, Джозеф А. и др. «Представляем объект». Программная инженерия с OBJ. Спрингер, Бостон, Массачусетс, 2000. 3–167.
- Месегер, Хосе. «Логика условного переписывания как единая модель параллелизма». Теоретическая информатика 96.1 (1992): 73–155.
- Гоген, Джозеф А. и Хосе Месегер. «Политики безопасности и модели безопасности». Симпозиум IEEE 1982 года по безопасности и конфиденциальности. ИИЭР, 1982.
Ссылки
[ редактировать ]- ^ «Хосе Месегер» . Проект «Математическая генеалогия» . Проверено 23 ноября 2022 г.
- ^ Jump up to: а б Марти-Олиет, Нарцисс; Ольцевски, Питер Чаба; Талкотт, Кэролин (2015). «Хосе Месегер: выдающийся ученый и друг». В Марти-Олиете — Нарцисс; Ольцевски, Питер Чаба; Талкотт, Кэролайн (ред.). Логика, переписывание и параллелизм: очерки, посвященные Хосе Месегеру по случаю его 65-летия . Спрингер. стр. 100-1 1–47. дои : 10.1007/978-3-319-23165-5 . ISBN 978-3-319-23164-8 . S2CID 46149140 .
- ^ «Профессор Хосе Месегер» . cs.illinois.edu . Проверено 28 апреля 2022 г.
- ^ Брох Йонсен, Эйнар (10 октября 2019 г.). «Стипендия FME присуждена профессору Хосе Месегеру» . fmeurope.org . Проверено 28 апреля 2022 г.
- ^ здесь отредактировано с учетом грамматики и стиля
- ^ «Стипендиаты ACM 2020 года отмечены за работу, которая лежит в основе современных компьютерных инноваций» . Ассоциация вычислительной техники . Нью-Йорк, штат Нью-Йорк. 13 января 2021 г. Проверено 23 ноября 2022 г.
- ^ Зейдлиц, Аарон (20 января 2021 г.). «ACM выражает признательность Месегеру Тонгу за вклад в область вычислений» . Новости . Университет Иллинойса . Проверено 23 ноября 2022 г.