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 |