 Nie jesteś zalogowany | zaloguj się |
| Nie jesteś zalogowany | zaloguj się |
2010-03-15, godz. 10:15, 4790
Patryk Czarnik (Uniwersytet Warszawski)
A dozen instructions make Java bytecode
Prerun przed Bytecode 2010.Abstrakt pracy: One of the biggest obstacles in the formalisation of the Java bytecode is that the language consists of 200 instructions. However, a rigorous handling of a programming language in the context of program verification and error detection requires a ...
2010-03-08, godz. 10:15, 4790
Aleksy Schubert (Uniwersytet Warszawski)
Aleksy opowie o wspólnej z Jackiem i Patrykiem pracy - sprowadzeniu całej funkcjonalności i wszystkich instrukcji Maszyny Wirtualnej Javy (JVM) do 12 instrukcji i zapisaniu operacyjnej semantyki małych kroków w postaci 23 reguł. Oczywiście instrukcje są sparametryzowane, aby móc reprezentow...
2010-03-01, godz. 10:15, 4790
Grzegorz Marczyński (Uniwersytet Warszawski)
O granicach w kategorii praporządków z morfizmami słabo odbijającymi domknięcia w dół
Podczas seminarium opowiem o moich zmaganiach z pokazaniem istnienia wszystkich granic w kategorii Preord!, której obiekty to praporządki, zaś morfizmy spełniają dwa warunki:(1) są monotoniczne(2) słabo odbijają domknięcia w dół, czyli dla f : A -> B, a\in A, b'\in B, jeśli b&#...
2010-01-18, godz. 10:15, 4790
Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)
Prerun wystąpienia na SofSem 2010
Będzie o automatycznym generowaniu anotacji, naszym narzędziu CodeStatistics i eksperymencie z pętlami for i decreases....
2010-01-11, godz. 10:15, 4790
Bartosz Zieliński (Wydział Fizyki i Informatyki Stosowanej, Uniwersytet Łódzki; Instytut Matematyki, PAN)
Polityki i modele kontroli dostępu - kontynuacja
Kontynuacja poprzedniego referatu, powtórka abstraktu: 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 macier...
2010-01-04, godz. 10:15, 4790
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 modyfika...
2009-12-14, godz. 10:15, 4790
Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)
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 zaprezentujemy numeryczne abstr...
2009-12-07, godz. 10:15, 4790
Artur Zawłocki (Uniwersytet Warszawski)
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 komponenty można połączyć przez sparowanie 'wyj...
2009-11-30, godz. 10:15, 4790
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ę programu. Z drug...
2009-11-16, godz. 10:15, 4790
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...
