Referaty w semestrze zimowym 12/13
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| O pracy magiserskiej | Z. Chlebicki | 17 XII 2012 | |
| O pracy magiserskiej | P. Iwaniuk | 12 XII 2012 | |
| P jest różne od NP nad nieskończonymi alfabetami | S. Lasota | 5 XII 2012 | |
| Języki bezkontekstowe nad nieskończonymi alfabetami | M. Maciejewska | 28 XI 2012 | |
| seminarium odwołane | 14 XI 2012 | ||
| Ograniczenia weryfikacji ograniczonej w narzędziu ESC/Java | Z. Chlebicki | 7 XI 2012 | |
| Automaty na nieskończonymi alfabetami | M. Maciejewska | 24 X 2012 | |
| Formalizacja protokołu Needhama-Schroedera | P. Iwaniuk | 17 X 2012 | |
| Formalizacja protokołu Needhama-Schroedera | P. Iwaniuk | 10 X 2012 |
Referaty w semestrze letnim 11/12
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| Temporal Linear Logic | J. Kopczewski | 6 VI 2012 | |
| Weryfikacja użycia pamięci | A. Morawski | 30 V 2012 | |
| WoW | 23 V 2012 | ||
| Ograniczona weryfikacja programów w C na przykładzie narzędzia CBMC | Z. Chlebicki | 16 V 2012 | |
| O pracy magisterskiej | M. Oniszczuk | 9 V 2012 | PDF |
| O pracy magisterskiej | J. Kopczewski | 25 IV 2012 | |
| Własności domknięcia automatów z więzami równościowymi | M. Maciejewska | 18 IV 2012 | PDF |
| Pixy czyli analiza statyczna aplikacji WWW | A. Morawski | 4 IV 2012 | PDF |
| SATABS czyli abstrakcja boolowska dla C | Z. Chlebicki | 28 III 2012 | |
| Needham-Schroeder w Coq'u | P. Iwaniuk | 21 III 2012 | PDF |
| Prover dla logiki liniowej | J. Kopczewski | 14 III 2012 | |
| HOOPL czyli analiza przeplywu danych w Haskell'u | M. Oniszczuk | 7 III 2012 | ODP |
| Delikatne wprowadzenie do JML'a | M. Maciejewska | 22 II 2012 | PDF |
Referaty w semestrze zimowym 11/12
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| 18 I 2012 | |||
| Zastosowanie logiki liniowej w opisie fabuł gier komputerowych | J. Kopczewski | 11 I 2012 | |
| Logika liniowa | J. Kopczewski | 4 I 2012 | |
| Logika BAN c.d. | P. Iwaniuk | 21 XII 2011 | PDF |
| Logika BAN | P. Iwaniuk | 14 XII 2011 | PDF |
| Gry fabularne | J. Kopczewski | 7 XII 2011 | |
| Prototypy aplikacji dla systemów wbudowanych | A. Morawski | 30 XI 2011 | WWW |
| Rachunek lambda + obiektowość c.d. | M. Oniszczuk | 23 XI 2011 | ODP |
| Rachunek lambda + obiektowość | M. Oniszczuk | 16 XI 2011 | ODP |
| Logika intuicjonistyczna | P. Iwaniuk | 9 XI 2011 | PDF |
| Case-study w UPPAALu | A. Morawski | 2 XI 2011 | |
| Gry fabularne | J. Kopczewski | 26 X 2011 |
Referaty w semestrze letnim 10/11
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| Frama-C | G. Anielak | 1 VI 2011 | WWW |
| Monte Carlo model checking | M. Pazurkiewicz i M. Sulikowski | 25 V 2011 | PDF |
| CADP | S. Rudnicki | 18 V 2011 | PDF |
| SLAM | B. Wołowiec i A. Morawski | 11 V 2011 | |
| Model Dolev-Yao i jego analiza | P. Iwaniuk | 4 V 2011 | |
| Analia statyczna programów w Python'ie | M. Oniszczuk | 20 IV 2011 | |
| Linux Driver Verification | M. Zielenkiewicz | 13 IV 2011 | |
| planowanie | 6 IV 2011 | ||
| Sprawdzanie równoważności programów - zastosowanie w narzędziu Codility | G. Anielak | 30 III 2011 | WWW |
| Analiza statyczna wskaźników w bajtkodzie Javy | M. Ziemba | 23 III 2011 | |
| Sprawdzanie funkcyjności metod Javy | S. Rudnicki | 16 III 2011 | PDF |
| Modelowanie sygnalizacji świetlnej w UPPAALu | M. Pazurkiewicz | 9 III 2011 | PDF |
| Weryfikacja procedur rekurencyjnych | M. Sulikowski | 2 III 2011 | PDF |
| O metrykach | A. Morawski | 23 II 2011 | WWW |
| Program slicing | B. Wołowiec | 16 II 2011 | PDF |
Referaty w semestrze zimowym 10/11
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| układamy plan | 19 I 2011 | ||
| Weryfikacja protokołów komunikacyjnych w systemach wieloagentowych | J. Iwaniuk | 12 I 2011 | |
| O narzędziach do odkrywania niezmienników | M. Zielenkiewicz | 5 I 2011 | |
| Model checking is static analysis of modal logic | M. Sulikowski | 15 XII 2010 | PDF |
| seminarium odwolane! | 8 XII 2010 | ||
| Formalna weryfikacja oprogramowania w lotnictwie | B. Wołowiec | 1 XII 2010 | PDF |
| L4.verified | A. Morawski | 24 XI 2010 | |
| Sprawdzanie równoważności programów | G. Anielak | 17 XI 2010 | |
| Automaty czasowe i UPPAAL | M. Pazurkiewicz | 10 XI 2010 | |
| Systemy hybrydowe | J. Iwaniuk | 3 XI 2010 | PDF |
| JSR 308 i weryfikacja adnotacji Javy | S. Rudnicki | 27 X 2010 | WWW |
| Analizator statyczny bajtkodu Javy | M. Ziemba | 20 X 2010 | PDF |
| Odkrywanie niezmienników | M. Zielenkiewicz | 13 X 2010 |
Referaty w semestrze letnim 09/10
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| Propozycje tematów prac magisterskich III | S. Lasota, A. Schubert | 2 czerwca 2010 | |
| Przydział zasobów w bazach danych | K. Błachnio | 19 maja 2010 | PDF |
| Binarny model checking | B. Zaborowski | 12 maja 2010 | WWW |
| Propozycje tematów prac magisterskich II | S. Lasota, A. Schubert | 5 maja 2010 | |
| Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking | G. Anielak | 5 maja 2010 | |
| Monte Carlo model checking | S. Rudnicki | 28 kwietnia 2010 | PDF |
| SMT - spełnialność z dokładnością do teorii | M. Pazurkiewicz | 21 kwietnia 2010 | |
| Propozycje tematów prac magisterskich I | S. Lasota, A. Schubert | 14 kwietnia 2010 | |
| Przyjazny interfejs dla gry weryfikacyjnej | G. Maj | 14 kwietnia 2010 | |
| O głośnych pluskwach | M. Ziemba | 31 marca 2010 | PDF |
| Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation | A. Morawski | 24 marca | WWW |
| Redukcja programów współbieżnych do sekwencyjnych przy ograniczonej liczbie zmian kontekstu | M. Sulikowski | 17 marca 2010 | PDF strona WWW narzędzia |
| Chess | J. Iwaniuk | 10 marca 2010 | PDF |
| Probabilistyczny model checking, PRISM i metody agregacyjne | M. Zakrzewska | 3 marca 2010 | |
| Testowanie za pomocą wykonywalnych projektów | M. Zielenkiewicz | 24 lutego 2010 | PDF zdjęcie |
Referaty w semestrze zimowym 09/10
| Temat referatu | Osoba referująca | Przybliżony termin | Materiały |
| KeY | M. Zielenkiewicz | 14 października 2009 | |
| [C]BMC | B. Zaborowski | 21 października 2009 | WWW |
| Splint | M. Ziemba | 28 października 2009 | |
| Temporalne własności systemów współbieżnych i model checking | K. Błachnio | 4 listopada 2009 | |
| Interfejs graficzny dla Concurrency Workbench | G. Maj | 18 listopada 2009 | WWW |
| Symboliczny model checking przy uzyciu BDD | B. Wołowiec | 25 listopada 2009 | |
| O interpretacji abstrakcyjnej | M. Pazurkiewicz | 2 grudnia 2009 | PS |
| Model checking: teoria automatow w praktyce | A. Zabłocki | 9 grudnia 2009 | |
| O pokryciu testami | G. Anielak | 16 grudnia 2009 | |
| JML-owe narzędzia ,,weryfikacji czasu wykonania'' | A. Morawski | 6 stycznia 2010 | WWW |
| Delta debugging | J. Iwaniuk | 13 stycznia 2010 | PDF |
| Model-checking programów w Javie | S. Rudnicki | 20 stycznia 2010 |
Referaty w semestrze letnim 08/09
| Temat referatu |
Osoba referująca |
Przybliżony termin |
Materiały |
| Abstrakcyjna interpretacja | Bartosz Zaborowski |
18 lutego 2009 |
|
| Abstrakcyjna interpretacja (cd) | Bartosz Zaborowski |
25 lutego 2009 |
WWW |
| nie odbyło się :( |
4 marca 2009 |
||
| O bisymulacji |
Grzegorz Maj |
11 marca 2009 |
PDF |
| O bisymulacji (cd) |
Grzegorz Maj |
18 marca 2009 |
PDF |
| JML |
Konrad Błachnio |
25 marca 2009 |
|
| JML (cd) |
Konrad Błachnio |
1 kwietnia 2009 |
|
| nie odbyło się :( |
8 kwietnia 2008 |
||
| Propozycje tematów prac magisterskich |
S.Lasota, A.Schubert |
22 kwietnia 2009 |
|
| Analiza przedzialowa |
Aleksander Zabłocki |
29 kwietnia 2009 |
|
| Analiza przedzialowa |
Aleksander Zabłocki |
6 maja 2009 |
PDF |
| Roztrzygalnosć logik modalnych |
Magda Zakrzewska |
13 maja 2009 |
PDF |
| Roztrzygalnosć logik modalnych (cd) |
Magda Zakrzewska |
20 maja 2009 |
|
| Weryfikacja programów wielowątkowych w Javie |
Aleksander Lewandowski |
27 maja 2009 |
PDF |
| O propozycjach tematów prac magisterskich |
S.Lasota, A.Schubert |
3 czerwca 2009 |
Referaty w semestrze zimowym 08/09
| Temat referatu |
Osoba referująca |
Przybliżony termin |
Materiały |
| AVISPA - narzędzie do weryfikacji protokołów kryptograficznych | Konrad Błachnio |
15 października 2008 |
|
| Metoda symbolicznej reprezentacji modeli - OBDD |
Grzegorz Maj |
22 października 2008 |
PDF |
| Podstawy JML-a |
Bartłomiej Bonarski |
29 października 2008 |
|
| O rozstrzygalności problemu stopu ;) |
Sławomir Lasota |
5 listopada 2008 |
|
| SAT-solvery |
Aleksander Lewandowski |
12 listopada 2008 |
|
| O narzędziu CBMC |
Aleksander Lewandowski |
19 listopada 2008 |
|
| Analiza kształtu z dobrym uporządkowaniem na listach |
Magda Zakrzewska |
26 listopada 2008 |
PDF |
| Analiza kształtu z dobrym uporządkowaniem na listach (cd) |
Magda Zakrzewska |
3 grudnia 2008 |
|
| Weryfikacja pamięci FLASH - case study |
Bartosz Zaborowski |
10 grudnia 2008 |
WWW |
| Automaty czasowe i Uppaal |
Aleksander Zabłocki |
17 grudnia 2008 |
PDF |
| Automaty czasowe i Uppaal (cd) |
Aleksander Zabłocki |
7 stycznia 2009 |
|
| Automaty czasowe a maszyny z błędami |
Paweł Kaczan |
14 stycznia 2009 |
|
| Automaty czasowe a maszyny z błędami (cd) |
Paweł Kaczan |
21 stycznia 2009 |