Informační systém Masarykovy univerzity 

Archiv závěrečné práce Milan Lenčo FI N-IN PDS

česky | in English

Agenda:
Změnit agendu. Adresa v ISu:

Masarykova univerzita

Fakulta informatiky

magisterský studijní program/obor:
Informatika/Paralelní a distribuované systémy

Práce na příbuzné téma

Zobrazit popisek

Bc. Milan Lenčo

Verification of Name Service Cache Daemon with DIVINE Model Checker

Anotace: V práci prezentujeme pokus o formálnu verifikáciu GNU nscd, unixového démona implementujúceho cache pre adresárové služby a dodávaného v rámci GNU C Library (glibc), s použitím nástroja na overovanie modelov DiVinE. Súčasne poskytujeme detailný popis všetkých krokov nevyhnutných k príprave a vykonaniu verifikácie netriviálnych C/C++ programov nástrojom DiVinE. V našom prístupe zachovávame zdrojový …více

Abstract: In this thesis we present an attempt to verify a number of important safety and liveness properties of GNU nscd, a name service cache daemon shipped alongside the GNU C Library, using the DiVinE model checker. We give a detailed description of all the steps needed to prepare and perform verification of a non-trivial C/C++ program with DiVinE. In our approach we keep nscd unmodified and wrap it around …více

divine nscd glibc nss model checking llvm software verification

Zadání: The GNU Name Service Cache Daemon (NSCD) provides a cache for common name service requests. The objective of the thesis is to investigate the feasibility of formal verification of NSCD using DiVinE model checker. Student will propose and implement a set of C/C++ unit tests simulating typical interaction with NSCD, while capturing a number of important safety and liveness properties of the cache, and …více

Jazyk práce: angličtina

  • Zadáno/změněno 11. 2. 2015 16:10, Helena Kryštofová
  • Záznam založen 9. 10. 2014 10:14, Miroslava Tomíčková
  • Zveřejnit od 6. 1. 2015 10:34, Miroslava Tomíčková
  • Práce převzata 6. 1. 2015 10:34, Miroslava Tomíčková

Obhajoba diplomové práce

  • Proběhla 11. 2. 2015, práce byla úspěšně obhájena.

Vedoucí:

  • prof. RNDr. Jiří Barnat, Ph.D., Sekr FI MU, Katedra teorie programování - Fakulta informatiky

Oponent:

Plný text práce
Příloha

Literatura:

  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999. xiv, 314. ISBN 0262032708.

Citační záznam

Citace dle ISO 690: LaTeX | HTML | text | BibTeX | Wikipedie

Kontrola závěrečné práce

Práce zkontrolována: 7. 1. 2015 12:09, prof. RNDr. Jiří Barnat, Ph.D.


Nástroje.Seřadit vzestupně.Seřadit sestupně. Spočítat nepřečtené soubory ve složkách. Spočítat velikost složek. Zobrazit mapu souborů. Napřed složky, pak soubory.Seřadit vzestupně.Seřadit sestupně. Složka či souborSeřadit vzestupně.Seřadit sestupně. Vložil/aSeřadit vzestupně.Seřadit sestupně. VloženoSeřadit vzestupně.Seřadit sestupně. Expirace: Seřadit vzestupně.Expirace: Seřadit sestupně.
Nástroje.Tato složka.  Archiv závěrečné práce Milan Lenčo FI N-IN PDS /fi_m/Tomíčková, M. 9. 10. 2014
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor annotation_english.txt, 979 B, holý textAnotace anglicky annotation_english.txtLenčo, M. 3.  1. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor annotation.txt, 1 KB, holý textAnotace česky annotation.txtLenčo, M. 3.  1. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor keywords.txt, 69 B, holý textKlíčová slova keywords.txtLenčo, M. 3.  1. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor dp-milan_lenco.pdf, 1 MB, PDF Soubor dp-milan_lenco.txt, 113,7 KB, holý textPlný text práce dp-milan_lenco.pdfLenčo, M. 3.  1. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor lenco_sxlbbrss.pdf, 49,1 KB, PDF Soubor lenco_sxlbbrss.txt, 1,4 KB, holý textPosudek oponenta lenco_sxlbbrss.pdfRočkai, P. 2.  2. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor lenco.pdf, 54,7 KB, PDF Soubor lenco.txt, 1,5 KB, holý textPosudek vedoucího lenco.pdfBarnat, J.22.  1. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor nscd-mc.tgz, 793,7 KB, archív GZIPPříloha nscd-mc.tgzLenčo, M. 3.  1. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Prohlédnout tuto složku po přihlášení do ISu (znáte-li svoje heslo do ISu, můžete zde vidět více souborů)

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 23. 9. 2017 18:27, 38. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému