 Nie jesteś zalogowany | zaloguj się |
| Nie jesteś zalogowany | zaloguj się |
2010-04-12, godz. 10:15, 4790
Michał R. Przybyłek (Uniwersytet Warszawski)
Na seminarium opowiem o swoich najnowszych pracach związanych z kateogryjnym podejściem do połączenia, zmieniających się wzdłuż ustalonego języka, świata teorii i świata modeli. Będzie o modułach, prorozwłóknieniach i kategoryzacji pojęcia instytucji....
2010-03-29, godz. 10:15, 4790
Tadeusz Sznuk (Uniwersytet Warszawski)
Generatory obligacji dowodowych
Zamierzam zacząc od powiedzenia, co to jest vcgen i jaką ma rolę w systemach weryfikacji. Potem omówię kilka takich systemów, w szczególności Vcc, Code contracts, KeY, Why, może też SPARK i Eiffel....
2010-03-22, godz. 10:15, 4790
Maciej Zielenkiewicz (Uniwersytet Warszawski)
Na seminarium pokazane zostanie, jak w naturalny sposób teoria kategorii (i topologia) znajdują zastosowanie w kwantowej teorii pola, pozwalając zarówno na ułatwienie obliczeń, jak i na budowę "uogólnionych" teorii. Przedstawione zagadnienia zostaną zilustrowane analogiami do z...
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...
