José Meseguer

José Meseguer
Urodzić się	1950 (wiek 72–73) Murcja , Hiszpania
Tytuł	Profesor, Informatyka
Nagrody	Stypendysta ACM 2020 2019 Formal Methods Europe Fellow
Wykształcenie
Alma Mater	Uniwersytet w Saragossie (doktorat)
Praca dyplomowa	Prymitywna rekurencja w kategoriach monoidalnych (1975)
Doradca doktorski	Michaela Pfendera
Praca akademicka
Dyscyplina	Informatyka
Instytucje	UIUC
Strona internetowa	http://formal.cs.illinois.edu/meseguer/

José Meseguer jest hiszpańskim informatykiem i profesorem na Uniwersytecie Illinois w Urbana-Champaign . Kieruje na uniwersytecie Pracownią Metod Formalnych i Języków Deklaratywnych.

Kariera

José Meseguer uzyskał doktorat z matematyki w 1975 r. na podstawie pracy zatytułowanej Rekurencja pierwotna w kategoriach modeli pod kierunkiem Michaela Pfendera na Uniwersytecie w Saragossie , po czym odbył staż podoktorancki na Uniwersytecie w Santiago de Compostela i Uniwersytecie Kalifornijskim w Berkeley . W 1980 roku dołączył do Laboratorium Informatyki w SRI International , ostatecznie zostając głównym naukowcem i kierownikiem działu logiki i deklaracji Grupa językowa. Dołączył do University of Illinois w 2001 roku i obecnie jest profesorem informatyki, gdzie kieruje laboratorium metod formalnych i języków deklaratywnych.

Pracował w szczególności nad projektowaniem i wdrażaniem języków deklaratywnych, w tym OBJ i Maude , a także przepisywaniem logiki.

Otrzymał stypendium Formal Methods Europe 2019 . W uzasadnieniu nagrody czytamy,

Za wszystkie jego osiągnięcia akademickie, przywództwo i wpływ na społeczność metod formalnych przedstawiamy prof. José Meseguera, stypendystę FME 2019. Prof. Meseguer jest czołowym naukowcem, który ma znaczący wkład w wiele dziedzin informatyki teoretycznej i nie tylko: od logiki ogólnej po algorytmy wizyjne dla robotów . Jego prace charakteryzują się innowacyjnością, konceptualną elegancją i rygorem w połączeniu z praktycznym zastosowaniem.

Prof. José Meseguer jest znany ze swoich przełomowych badań nad specyfikacjami algebraicznymi , współbieżnością , przepisywaniem , logiką i bezpieczeństwem komputerowym . Badania naszego nowego stypendysty charakteryzują się praktyczną, prostą i intuicyjną logiką obliczeniową oraz powiązanymi metodami i narzędziami analitycznymi. Wyniki badań zostały z powodzeniem zastosowane w złożonych, najnowocześniejszych systemach w różnych dziedzinach.

Jego praca nad bezpieczeństwem komputerowym jest szczególnie znacząca. Jego sformalizowanie nieingerencji jest jedną z najbardziej znanych koncepcji bezpieczeństwa komputerowego, szeroko stosowaną zarówno przez naukowców, jak i praktyków. Jego artykuł na temat zasad bezpieczeństwa i modeli bezpieczeństwa jest jednym z najczęściej cytowanych artykułów w dziedzinie bezpieczeństwa komputerowego (z prawie 2500 cytatami z Google Scholar ).

Pracował nad projektowaniem i wdrażaniem kilku języków deklaratywnych , w tym OBJ i Maude , nad formalną specyfikacją i technikami weryfikacji , nad teorią współbieżności , nad formalnym podejściem do specyfikacji zorientowanej obiektowo, nad równoległym oprogramowaniem i architekturami dla języków deklaratywnych oraz nad logiczne podstawy informatyki z wykorzystaniem logiki równań , przepisywania logiki i teorii logiki ogólnej.

Jest wynalazcą przepisywania logiki i głównym twórcą Maude. Jego fundamentalnym wkładem w metody formalne było wynalezienie i rozwój przepisywania jako ekspresyjnej i intuicyjnej logiki obliczeniowej oraz semantycznej dla systemów współbieżnych. W szczególności zestaw narzędzi Maude jest praktycznym, wydajnym narzędziem do przepisywania.

Ważnym wynikiem jest wykazanie, że przepisywanie logiki jest naturalnym i prostym modelem współbieżności. Prostota i wyrazistość przepisywania logiki, zaimplementowana w Maude, zaowocowała specyfikacją i analizą szerokiej gamy systemów, w tym modeli obliczeniowych , różnych logik, programowania przemysłowego i języków modelowania .

Wniósł również fundamentalny wkład w formalną analizę systemów rozproszonych , łącząc rozumowanie oparte na stanie i działanie w logice temporalnej ; łączenie przepisywania z rozwiązywaniem SMT ; oraz zapewnienie ogólnych algorytmów rozwiązywania teorii SMT, które można zastosować nie tylko do ustalonych predefiniowanych teorii, ale do dowolnej teorii, która spełnia określone właściwości. Nowsze wkłady badawcze obejmują systemy cyber-fizyczne , przetwarzanie w chmurze i systemy biologiczne .

Jego naukowe podejście najlepiej opisuje powiedzenie „piękno to nasza sprawa”. Nie boi się zapuszczać w domenę odległą od tego, co uznalibyśmy za jego strefę komfortu; w rzeczywistości rozkoszuje się możliwością narzucenia rygoru innym dziedzinom i sprostania nowym wyzwaniom, które inspirują nowe rozwiązania teoretyczne.

Świadectwa przyjaciół i współpracowników, że stara się zachować najwyższe standardy etyczne i naukowe w swoich badaniach oraz w kontaktach z kolegami, studentami i innymi ludźmi wokół siebie. Nowi studenci są traktowani z taką samą uprzejmością jak czołowi badacze. Znajduje to odzwierciedlenie w fakcie, że wielu byłych studentów kontynuuje współpracę, gdy stają się starszymi naukowcami.

Jest niezwykle hojny w dzieleniu się i omawianiu wielu pomysłów pochodzących z jego płodnego umysłu i jest naprawdę ciekawy i docenia inne opinie. Świadkiem tego ducha współpracy jest również posiadanie przez niego 132 współautorów notowanych na DBLP . Pomimo tego, że jest jednym z czołowych informatyków naszego pokolenia, wielu jego współpracowników uważa go przede wszystkim za niezwykle lojalnego i prawdziwego przyjaciela.

Został wprowadzony jako stypendysta ACM w 2020 r. „Za rozwój metod logicznych projektowania i weryfikacji systemów obliczeniowych”.

Wybrane badania

• Clavel, Manuel i in. Wszystko o Maude — wysokowydajna struktura logiczna: jak określać, programować i weryfikować systemy w przepisywaniu logiki. Springer-Verlag, 2007.
• Goguen, Joseph A. i in. „Przedstawiamy obiekt”. Inżynieria oprogramowania z OBJ. Springer, Boston, MA, 2000. 3–167.
• Meseguer, José. „Logika warunkowego przepisywania jako ujednolicony model współbieżności”. Informatyka teoretyczna 96.1 (1992): 73–155.
• Goguen, Joseph A. i José Meseguer. „Polityki bezpieczeństwa i modele bezpieczeństwa”. 1982 Sympozjum IEEE na temat bezpieczeństwa i prywatności. IEEE, 1982.