Organizatorzy

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

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

14 grudnia 2009 10:15
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 …
7 grudnia 2009 10:15
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 …
30 listopada 2009 10:15
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ę …
16 listopada 2009 10:15
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 …
9 listopada 2009 10:15
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 …
2 listopada 2009 10:15
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 …
26 października 2009 10:15
Aleksy Schubert (Uniwersytet Warszawski)
Prerun wystąpień w Eindhoven
19 października 2009 10:15
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 …
12 października 2009 10:15
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 …
5 października 2009 10:15
- (Uniwersytet Warszawski)
Spotkanie organizacyjne, ustalanie tematów referatów.
4 maja 2009 10:15
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 …
27 kwietnia 2009 10:15
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 …
30 marca 2009 10:15
Artur Zawłocki (Uniwersytet Warszawski)
Formalizm do specyfikacji komponentów w oparciu o logikę liniowo-temporalną -- work in progress
23 marca 2009 10:15
prof. Andrzej Tarlecki (Uniwersytet Warszawski)
Heterogeniczne środowiska logiczne - spojrzenie instytucyjne
16 marca 2009 10:15
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. …
8 grudnia 2008 10:15
Ł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 …
17 listopada 2008 10:15
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 …
3 listopada 2008 10:15
Patryk Czarnik (Instytut Informatyki, Uniwersytet Warszawski)
Ku abstrakcyjnemu podejściu do weryfikacji bajtkodu Javy
27 października 2008 10:15
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).
20 października 2008 10:15
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 …