Memory Representation for Model Checker of C/C++
We describe the design and C++ implementation of the newly created memory module (MM) in this work. It will be used in the GIMPLE Model Checker, an explicit state model checker, to represent the memory of checked program. MM diers from other code model checkers in the fact, that it stores ordinary C...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Dissertation |
| Language: | English |
| Published: |
2010
|
| Online Access: | http://www.nusl.cz/ntk/nusl-286282 |