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. |