Nie jesteś zalogowany | Zaloguj się
Powrót do listy seminarów

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze.

Strona domowa: https://www.mimuw.edu.pl/~alx/piatek.html


Organizatorzy

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

  • 4 stycznia 2010 10:15
    Bartosz Zieliński (Wydział Fizyki i Informatyki Stosowanej, Uniwersytet Łódzki; Instytut Matematyki, PAN)
    Polityki i modele kontroli dostępu
    Omówione zostaną podstawowe pojęcia związane z bezpieczeństwem, modele kontroli dostępu, polityki bezpieczeństwa i związane z nimi problemy, m.in: rozróżnienie na uznaniową i obowiązkową kontrolę dostępu, podstawowy model macierzy dostępu, model Harisona-Ruzzo-Ullmana i jego modyfikacje, nierozstrzygalność …

  • 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 …


  • 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 …