Témata prací (Výběr práce)Témata prací (Výběr práce)(verze: 348)
Detail práce
   Přihlásit přes CAS
Memory Representation for Model Checker of C/C++
Název práce v češtině: Memory Representation for Model Checker of C/C++
Název v anglickém jazyce: Memory Representation for Model Checker of C/C++
Akademický rok vypsání: 2008/2009
Typ práce: diplomová práce
Jazyk práce: angličtina
Ústav: Katedra softwarového inženýrství (32-KSI)
Vedoucí / školitel: RNDr. Ondřej Šerý, Ph.D.
Řešitel: skrytý - zadáno a potvrzeno stud. odd.
Datum přihlášení: 21.10.2008
Datum zadání: 21.10.2008
Datum a čas obhajoby: 02.02.2010 00:00
Datum odevzdání elektronické podoby:02.02.2010
Datum proběhlé obhajoby: 02.02.2010
Oponenti: doc. RNDr. Jan Kofroň, Ph.D.
 
 
 
Zásady pro vypracování
A code model checker is a tool for analysis of program source codes. It identifies potential flaws via
exhaustive exploration of the relevant portion of the program state space. An integral part of such
a tool is representation of the program's memory. This task becomes challenging for source languages
featuring support for untyped heap allocation (e.g., as C/C++).

In the scope of the thesis, an extensible module for representation of program memory will be designed
and implemented based on the existing related work [1,2]. The module would support incremental heap
canonicalization (implementation of an existing algorithm), tagged memory cells (based on the last stored
type).

Summary of thesis goals:
(i) Study of related work
(ii) Design of an extensible memory representation module
(iii) Implementation of the module in C++
Seznam odborné literatury
[1] Musuvathi, M., Dill, D. L.: An Incremental Heap Canonicalization Algorithm, in Model Checking Software, LNCS 3639, 2005.

[2] Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs, in Automated Software Engineering Journal, vol. 10, num. 2, 2003.

[3] Clarke, E. M., Grumberg, o., Peled, D. A.: Model Checking, MIT Press, 1999.
 
Univerzita Karlova | Informační systém UK