Organizers

dr hab. Aleksy Schubert, prof. UW
prof. dr hab. Andrzej Tarlecki
prof. dr hab. Paweł Urzyczyn

Information

Fridays, 12:15 p.m. , room: 5450

Research fields

List of talks

Dec. 14, 2009, 10:15 a.m.
Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)
Analiza abstrakcyjna
Na seminarium opowiemy o wykorzystaniu abstrakcyjnej interpretacji do analizy kodu programów. Skupimy się na zastosowaniu jej do sprawdzania występowania błędów rzepełnienia zakresu liczb całkowitych oraz wyjścia poza zakres tablicy w języku Java. W tym celu …
Dec. 7, 2009, 10:15 a.m.
Artur Zawłocki (Uniwersytet Warszawski)
Doktorat
Opowiem o formalizmie, mojego autorstwa, do opisu systemów zbudowanych z komponentów, z których każdy porozumiewa się z otoczeniem za pośrednictwem akcji. Podobnie jak np. w CCS i CSP, komunikacja odbywa się przez synchronizację akcji: dwa …
Nov. 30, 2009, 10:15 a.m.
Piotr Kosiuczenko
Efektywna implementacja operatora @pre/old i jej weryfikacja
Referat dotyczy implementacji operatorów zwracających wartość parametru sprzed wykonania operacji takich jak @pre w języku OCL oraz \old w językach JML i Spec#. Dotychczasowe implementacje nie gwarantowały żadnych ograniczeń czasowych, a nawet własności zatrzymywania się …
Nov. 16, 2009, 10:15 a.m.
Grzegorz Marczyński (Uniwersytet Warszawski)
Sygnatury algebraiczne z porządkiem na symbolach
Na seminarium przedstawię wyniki mojej pracy nad sygnaturami algebraicznymi, które zawierają relację zależności pomiędzy symbolami. Pokażę też definicję kategorii fragmentów takich sygnatur, pullback-pushout uzupełnień, oraz kilku funktorów służących do "domykania" fragmentów w całości. Do tego …
Nov. 9, 2009, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Co się działo na drugim światowym kongresie Formal Methods
Duże konferencje wyznaczają zwykle trendy w badaniach nad danym tematem. Zwłaszcza dotyczy to zaproszonych wykładów. Na referacie zaprezentuję streszczenie zaproszonych wykładów: + Formal Methods for Privacy, Jeanette Wing + What can Formal Methods bring do …
Nov. 2, 2009, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
O weryfikacji bajtkodu Javy
Weryfikacja bajtkodu to operacja wykonywana przez większość impementacji Maszyny Wirtualnej Javy podczas ładowania klas, której celem jest sprawdzenie poprawności bajtkodu, ze szczególnym uwzględnieniem zgodności typów argumentów dla poszczególnych instruckji JVM. Na seminarium opowiem o własnych …
Oct. 26, 2009, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Prerun wystąpień w Eindhoven
Oct. 19, 2009, 10:15 a.m.
Aleksy Schubert i Jacek Chrząszcz (Uniwersytet Warszawski)
Weryfikacja skompilowanych klas Javy w oparciu o specyfikację w BML - studium przypadku
W ramach zakończonego niedawno projektu Mobius powstało szereg narzędzi do specyfikacji i weryfikacji własności programów w Javie. Jednym z narzędzi jest generator obligacji dowodowych BMLVCGen, który na podstawie pliku ze skompilowaną klasą Javy wzbogaconą o …
Oct. 12, 2009, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
Szkoła letnia ISS-AiPL
W sierpniu miałem przyjemność w Edynburgu brać udział w szkole International Summer School on Advances in Programming Languages http://www.macs.hw.ac.uk/~greg/ISS-AiPL/ Na seminarium postaram się streścić 10 wykładów Szkoły :), a tak naprawdę zapewne uda się nieco …
Oct. 5, 2009, 10:15 a.m.
- (Uniwersytet Warszawski)
Spotkanie organizacyjne, ustalanie tematów referatów.
May 4, 2009, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
Abstrakcyjne podejście do weryfikacji bajtkodu Javy
Weryfikacja bajtkodu to czynność przeprowadzana przez większość implementacji maszyny wirtualnej Javy podczas ładowania bajtkodu, w celu sprawdzenia poprawności programu przed jego uruchomieniem. W trakcie weryfikacji, w celu sprawdzenia poprawności typowej, przeprowadzana jest m.in. statyczna analiza …
April 27, 2009, 10:15 a.m.
Grzegorz Marczyński i Artur Zawłocki (Uniwersytet Warszawski)
A Heterogeneous Approach to Service-Oriented Systems Specification: Two Months Later
Service-oriented architecture (SOA) is a relatively new ap- proach to software system development. It divides system functionality to independent, loosely coupled, interoperable services. In this paper we propose a new heterogeneous specification approach of SOA …
March 30, 2009, 10:15 a.m.
Artur Zawłocki (Uniwersytet Warszawski)
Formalizm do specyfikacji komponentów w oparciu o logikę liniowo-temporalną -- work in progress
March 23, 2009, 10:15 a.m.
prof. Andrzej Tarlecki (Uniwersytet Warszawski)
Heterogeniczne środowiska logiczne - spojrzenie instytucyjne
March 16, 2009, 10:15 a.m.
prof. Andrzej Tarlecki (Uniwersytet Warszawski)
Heterogeniczne środowiska logiczne - spojrzenie instytucyjne
HETEROGENEOUS LOGICAL ENVIRONMENTS: AN INSTITUTIONAL VIEW We work within the theory of institutions as a framework where the theory of specification and formal software development may be presented in an adequately general and abstract way. …
Dec. 8, 2008, 10:15 a.m.
Łukasz Jancewicz (Uniwersytet Warszawski)
Anonimowość w BitTorrencie
BitTorrent jest obecnie najpopularniejszym protokołem peer-to-peer, czyli służącym do bezpośredniej wymiany plików między użytkownikami Internetu. Przyczyną takiej popularności jest jego szybkość i skalowalność, które osiąga się kosztem m.in. prywatności. W ostatnich latach, głównie z powodu …
Nov. 17, 2008, 10:15 a.m.
Piotr Kosiuczenko
Przepisywanie termów jako semantyczna podstawa modelowania graficznego
Graficzne języki modelowania, takie jak Unified Modeling Language (UML) i Specification and Description Language (SDL), są dziś powszechnie stosowane w praktyce inżynierii oprogramowania. Jednakże ich rozwój wymagał lat pracy nad notacjami w nich zawartymi oraz …
Nov. 3, 2008, 10:15 a.m.
Patryk Czarnik (Instytut Informatyki, Uniwersytet Warszawski)
Ku abstrakcyjnemu podejściu do weryfikacji bajtkodu Javy
Oct. 27, 2008, 10:15 a.m.
Grzegorz Marczyński (Uniwersytet Warszawski)
BPMN, czyli Business Process Modeling Notation
Na seminarium na przykładach przedstawię notację BPMN w wersji 1.1. Postaram sie również opisać związki pomiędzy BPMN i BPEL (Business Process Execution Language).
Oct. 20, 2008, 10:15 a.m.
Artur Zawłocki (Uniwersytet Warszawski, Instytut Informatyki)
An Algebraic Semantics for Contract-based Software Components
Praca Michela Bidoit i Rolfa Hennickera (z AMAST 2008) Abstrakt pracy: We propose a semantic foundation for the contract-based design of software components. Our approach focuses on the characteristic principles of component-oriented development, like provided …