Informační systém Masarykovy univerzity 

Archiv závěrečné práce Vladimír Štill 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. Vladimír Štill

LLVM Transformations for Model Checking

LLVM Transformations for Model Checking

Anotace: Tato práce je zaměřená na využití LLVM transformací jako kroku, který je předřazen verifikaci programů v programovacích jazycích C a C++ s pomocí nástroje pro explicitní model checking DIVINE. Práce demonstruje, že LLVM transformace mohou být použity jak pro rozšíření schopností verifikačního nástroje, tak i pro redukci velikosti stavového prostoru. Co se rozšíření schopností verifikačního nástroje …více

Abstract: This work focuses on application of LLVM transformations as a preprocessing step for verification of real-world C and C++ programs using the explicit-state model checker DIVINE. We demonstrate that LLVM transformations can be used for extension of verifier capabilities and for reduction of the state space size. In the case of extension of verifier capabitilies, the main focus is on verification under …více

Formal Verification C C++ LLVM Model Checking Parallel DIVINE LART LLVM Transformation Weak Memory Models Total Store Order Implementation

Zadání: When model checking a C++ program with an explicit-state model checker DIVINE, the input program is first translated to an LLVM bitcode that serves as an input formalism for the model checker. The goal of this thesis is to explore possibilities of LLVM bitcode to LLVM bitcode transformations that could either improve or extend capabilities of the model checker. It is expected that within the thesis …více

Jazyk práce: angličtina

  • Zadáno/změněno 15. 2. 2016 16:08, Helena Kryštofová
  • Záznam založen 7. 12. 2015 10:06, Pavla Wolfová
  • Zveřejnit od 11. 1. 2016 08:53, Eva Drštková
  • Práce převzata 11. 1. 2016 08:53, Eva Drštková

Obhajoba diplomové práce

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

Vedoucí:

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

Oponent:

  • doc. RNDr. Jan Strejček, Ph.D., KTP FI MU, Institut teoretické informatiky - Fakulta informatiky
Plný text práce
Příloha
  • Příloha Příloha Mgr. Vladimír Štill (stud FI MU)

Citační záznam

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

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

Práce zkontrolována: 13. 1. 2016 08:02, 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 Vladimír Štill FI N-IN PDS /fi_m/Wolfová, P. 7. 12. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor annotation_english.txt, 1 KB, holý textAnotace anglicky annotation_english.txtŠtill, V.10.  1. 2016
Čí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.txtŠtill, V.11.  1. 2016
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor keywords.txt, 149 B, holý textKlíčová slova keywords.txtŠtill, V.10.  1. 2016
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor thesis.pdf, 506,3 KB, PDF Soubor thesis.txt, 180,6 KB, holý textPlný text práce thesis.pdfŠtill, V.10.  1. 2016
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor posudek_oponenta_Strejcek.pdf, 49,7 KB, PDF Soubor posudek_oponenta_Strejcek.txt, 2 KB, holý textPosudek oponenta posudek_oponenta_Strejcek.pdfStrejček, J. 8.  2. 2016
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor posudek_vedouciho_Barnat.pdf, 96,3 KB, PDF Soubor posudek_vedouciho_Barnat.txt, 1,5 KB, holý textPosudek vedoucího posudek_vedouciho_Barnat.pdfBarnat, J. 5.  2. 2016
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor llvmtrans.tar.gz, 27,3 MB, archív GZIPPříloha llvmtrans.tar.gzŠtill, V.10.  1. 2016
Čí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:26, 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