Weryfikacja wspomagana komputerowo lato 2014/15
| Język wykładowy | Angielski |
|---|---|
| Opiekun | Witold Charatonik |
| Liczba godzin | |
| Rodzaj | I2.T - teoria inf. |
| ECTS | 6 |
| Polecany dla I roku | Nie |
| Egzamin | Tak |
Opis przedmiotu:
Wykład prowadzony wspolnie z Małgorzatą Biernacką. Wykład będzie poświęcony przeglądowi metod weryfikacji systemow komputerowych, rozumianych zarowno jako sprzęt jak i oprogramowanie. Oprocz podstaw teoretycznych poznamy także najbardziej popularne narzędzia weryfikacji. Wykład będzie się składał z dwoch części. W pierwszej z nich zajmiemy się weryfikacją modelową. Opowiemy o logikach temporalnych (LTL, CTL), o problemie sprawdzania modelu (and. model checking), o metodach radzenia sobie z problemem eksplozji przestrzeni stanow - o podejściu symbolicznym z użyciem efektywnych struktur danych (OBDD), o ograniczonej weryfikacji modelowej (ang. bounded model checking) z zastosowaniem SAT-solverow, o abstrahowaniu. Poznamy narzędzia takie jak NuSMV. W drugiej części wykładu zajmiemy się weryfikacją dedukcyjną programow. Omowimy podstawy klasycznej logiki Hoare'a oraz jej zastosowanie do automatycznej weryfikacji programow. Następnie zajmiemy się wspołczesnym rozszerzeniem logiki Hoare'a - logiką separacji (ang. separation logic) służącą do lokalnego wnioskowania o stanie sterty, niezbędnego w weryfikacji programow manipulujących wskaźnikami. Omowimy wybrane zastosowania i rozszerzenia logiki separacji. W części praktycznej zapoznamy się z wybranymi narzędziami wspomagającymi wnioskowanie dedukcyjne.Wykłady
Lista| Prowadzący | Termin zajęć | Limit | Zapisani | Kolejka |
|---|---|---|---|---|
|
Witold Charatonik
english |
cz 12:00-14:00 (s. 139) | 300 | 13 | 0 |
|
Małgorzata Biernacka
english |
cz 12:00-14:00 (s. 139) | 0 | 13 | 0 |
UWAGA! Wyższa liczba oznacza wyższy priorytet, po zapisaniu do grupy zostajemy usunięci z kolejek o niższym priorytecie.
Ćwiczenia
Lista| Prowadzący | Termin zajęć | Limit | Zapisani | Kolejka |
|---|---|---|---|---|
|
Witold Charatonik
english |
cz 14:00-16:00 (s. 139) | 20 | 13 | 0 |
|
Małgorzata Biernacka
english |
cz 14:00-16:00 (s. 139) | 0 | 0 | 0 |
UWAGA! Wyższa liczba oznacza wyższy priorytet, po zapisaniu do grupy zostajemy usunięci z kolejek o niższym priorytecie.
Konsultacje prowadzących:
| Imię i nazwisko | Pokój | Konsultacje |
|---|---|---|
| Małgorzata Biernacka | 348 | wt., pt. 13-14 + możliwe inne terminy, po wcześniejszym umówieniu się |
| Witold Charatonik | 347 | wtorek 14-16 lub po indywidualnym uzgodnieniu terminu (semestr letni 2024) |