Page 12 - GP_02_2010
P. 12
RODY
Na zdjęciu: dr inż. hab Teofil Jesionowski (piąty
z lewej) i dr inż. hab. Paweł T. Wojciechowski
(trzeci z prawej) podczas wręczenia nagród.
NAGRODY modularnych z możliwością dyna-
micznej zmiany protokołów (SA-
IV WYDZIAŁU NAUK TECHNICZNYCH PAN MOA). Zaprojektował i zaimplemen-
tował język Nomdic Pict, który jest
27listopada 2009 r. prze- z Politechniką Poznańską, prowa- silnie typowany – kompilator prze-
wodniczący Wydziału IV dzi zajęcia z przedmiotu „Systemy prowadza statyczną weryfikację
Nauk Technicznych PAN typów dla języków programowa- zgodności typów w programach,
prof. dr hab. Władysław Włosiński nia”. Zajmuje się systemami infor- co pozwala na wykrycie błędnego
wręczył nagrody siedmiu naukow- matycznymi, semantyką języków zastosowania konstrukcji języka.
com, których prace zostały zgłoszo- programowania, systemami typów, W celu weryfikacji programów
ne do tegorocznej edycji konkursu. teorią współbieżności oraz syste- rozproszonych zawierających kon-
Wśród grona nagrodzonych znaleźli mami rozproszonymi. Jego badania strukcję Nomadic Pict dr hab. inż.
się przedstawiciele Politechniki Po- dotyczyły fundamentalnych pod- Wojciechowski rozszerzył definicje
znańskiej: dr hab. inż. Teofil Jesio- staw, a także praktycznych aspek- statycznego systemu typów zapoży-
nowski oraz dr hab. inż. Paweł T. tów systemów współbieżnych, roz- czoną z języka Pict oraz zastosował
Wojciechowski. proszonych oraz mobilnych. Celem odpowiednie mechanizmy statycz-
badań jest opracowanie języków nej weryfikacji typów jako warstwę
Dr hab. inż. Paweł T. Wojciechow- programowania nowej generacji kompilatora Nomadic Pict. Cechą
ski, Instytut Informatyki, Wydział oraz narzędzi weryfikacji popraw- wyróżniającą projekt Nomadic Pict
Informatyki i Zarządzania PP. za ności programów, które mogłyby było to, że definicja opracowane-
rozprawę habilitacyjną „ Lanuage usprawnić implementacje powyż- go języka jest w pełni formalna.
Design for Automicity, Declarati- szych systemów z gwarancjami W tym celu dr hab. inż. Wojcie-
ve Synchronization, and Dynamic bezpieczeństwa i niezawodności. chowski zdefiniował rachunek pro-
Update in Comunicating Systems” Zajmował się również językiem cesów Nomadic ϖ, który jest roz-
otrzymał Nagrodę IV Wydziału Nauk operacji atomowych i deklaratyw- szerzeniem rachunku ϖ o abstrakcję
Technicznych PAN. nej synchronizacji, obiektowym ję- programowania rozproszonego
zykiem dynamicznych wiązań oraz i konstrukcję do tworzenia, migracji
Od 1993 r. zawodowo związany narzędziami do budowy protokołów i komunikacji mobilnych agentów.
Semantyka operacyjna rachunku
Nomadic ϖ pozwoliła na precyzyjną
specyfikę wszystkich konstrukcji
języka i algorytmów infrastruktu-
ry komunikacyjnej, zakodowanych
w Nomadic Pict oraz umożliwia for-
malne dowodzenie ich poprawno-
ści. Typowany rachunek Nomadic ϖ
wraz z jego rozszerzeniami o meto-
dy wnioskowania został użyty przez
niego do formalnego udowodnie-
nia, że przykładowe, zaprojektowa-
ne przez dra algorytmy infrastruk-
tury komunikacyjnej są faktycznie
prawidłowe (algorytmy te stanowią
część dystrybucji Nomadic Pict).
Zanim zaprojektował własny model
i framework do takiej kompozycji,
opisał formalnie semantykę kon-
strukcji w trzech istniejących fra-
meworkach protokołowych (Cac-
tus, X-kernel, Appia). W ramach
realizowanego przez niego projektu
12 | GŁOS POLITECHNIKI | LUTY 2010
Na zdjęciu: dr inż. hab Teofil Jesionowski (piąty
z lewej) i dr inż. hab. Paweł T. Wojciechowski
(trzeci z prawej) podczas wręczenia nagród.
NAGRODY modularnych z możliwością dyna-
micznej zmiany protokołów (SA-
IV WYDZIAŁU NAUK TECHNICZNYCH PAN MOA). Zaprojektował i zaimplemen-
tował język Nomdic Pict, który jest
27listopada 2009 r. prze- z Politechniką Poznańską, prowa- silnie typowany – kompilator prze-
wodniczący Wydziału IV dzi zajęcia z przedmiotu „Systemy prowadza statyczną weryfikację
Nauk Technicznych PAN typów dla języków programowa- zgodności typów w programach,
prof. dr hab. Władysław Włosiński nia”. Zajmuje się systemami infor- co pozwala na wykrycie błędnego
wręczył nagrody siedmiu naukow- matycznymi, semantyką języków zastosowania konstrukcji języka.
com, których prace zostały zgłoszo- programowania, systemami typów, W celu weryfikacji programów
ne do tegorocznej edycji konkursu. teorią współbieżności oraz syste- rozproszonych zawierających kon-
Wśród grona nagrodzonych znaleźli mami rozproszonymi. Jego badania strukcję Nomadic Pict dr hab. inż.
się przedstawiciele Politechniki Po- dotyczyły fundamentalnych pod- Wojciechowski rozszerzył definicje
znańskiej: dr hab. inż. Teofil Jesio- staw, a także praktycznych aspek- statycznego systemu typów zapoży-
nowski oraz dr hab. inż. Paweł T. tów systemów współbieżnych, roz- czoną z języka Pict oraz zastosował
Wojciechowski. proszonych oraz mobilnych. Celem odpowiednie mechanizmy statycz-
badań jest opracowanie języków nej weryfikacji typów jako warstwę
Dr hab. inż. Paweł T. Wojciechow- programowania nowej generacji kompilatora Nomadic Pict. Cechą
ski, Instytut Informatyki, Wydział oraz narzędzi weryfikacji popraw- wyróżniającą projekt Nomadic Pict
Informatyki i Zarządzania PP. za ności programów, które mogłyby było to, że definicja opracowane-
rozprawę habilitacyjną „ Lanuage usprawnić implementacje powyż- go języka jest w pełni formalna.
Design for Automicity, Declarati- szych systemów z gwarancjami W tym celu dr hab. inż. Wojcie-
ve Synchronization, and Dynamic bezpieczeństwa i niezawodności. chowski zdefiniował rachunek pro-
Update in Comunicating Systems” Zajmował się również językiem cesów Nomadic ϖ, który jest roz-
otrzymał Nagrodę IV Wydziału Nauk operacji atomowych i deklaratyw- szerzeniem rachunku ϖ o abstrakcję
Technicznych PAN. nej synchronizacji, obiektowym ję- programowania rozproszonego
zykiem dynamicznych wiązań oraz i konstrukcję do tworzenia, migracji
Od 1993 r. zawodowo związany narzędziami do budowy protokołów i komunikacji mobilnych agentów.
Semantyka operacyjna rachunku
Nomadic ϖ pozwoliła na precyzyjną
specyfikę wszystkich konstrukcji
języka i algorytmów infrastruktu-
ry komunikacyjnej, zakodowanych
w Nomadic Pict oraz umożliwia for-
malne dowodzenie ich poprawno-
ści. Typowany rachunek Nomadic ϖ
wraz z jego rozszerzeniami o meto-
dy wnioskowania został użyty przez
niego do formalnego udowodnie-
nia, że przykładowe, zaprojektowa-
ne przez dra algorytmy infrastruk-
tury komunikacyjnej są faktycznie
prawidłowe (algorytmy te stanowią
część dystrybucji Nomadic Pict).
Zanim zaprojektował własny model
i framework do takiej kompozycji,
opisał formalnie semantykę kon-
strukcji w trzech istniejących fra-
meworkach protokołowych (Cac-
tus, X-kernel, Appia). W ramach
realizowanego przez niego projektu
12 | GŁOS POLITECHNIKI | LUTY 2010
