Survey of memory modeling methods in static verification tools
The paper presents a survey of existing approaches to modeling memory states of C programs with SMT-formulas in context of static verification. The paper highlights the essential problems of C memory model development and describes two major groups of C memory models: one comprising of models that s...
| Váldodahkkit: | , |
|---|---|
| Materiálatiipa: | Artihkal |
| Giella: | English |
| Almmustuhtton: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Ráidu: | Труды Института системного программирования РАН |
| Fáttát: | |
| Liŋkkat: | https://ispranproceedings.elpub.ru/jour/article/view/240 |
| _version_ | 1828425210047496192 |
|---|---|
| author | M. U. Mandrykin V. S. Mutilin |
| author_facet | M. U. Mandrykin V. S. Mutilin |
| author_sort | M. U. Mandrykin |
| collection | DOAJ |
| description | The paper presents a survey of existing approaches to modeling memory states of C programs with SMT-formulas in context of static verification. The paper highlights the essential problems of C memory model development and describes two major groups of C memory models: one comprising of models that support unbounded memory regions and another including the models that don’t. Among the models for a priori bounded memory regions the paper discusses a strongest postcondition-based model relying on preliminary alias analysis and a weakest precondition-based model that uses uninterpreted functions and first-order logic to represent pointer predicates. Among the models for unbounded memory areas the paper describes a typed memory model, the Burstall-Bornat model, a region-based model and a model with full support for the Logic of Interpreted Sets and Bounded Quantification (LISBQ) earlier implemented in the HAVOC deductive verification tool. |
| first_indexed | 2024-12-10T16:29:20Z |
| format | Article |
| id | doaj.art-a55de7ac261647ad89b8ab10b791bc58 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-10T16:29:20Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-a55de7ac261647ad89b8ab10b791bc582022-12-22T01:41:35ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0129119523010.15514/ISPRAS-2017-29(1)-12240Survey of memory modeling methods in static verification toolsM. U. Mandrykin0V. S. Mutilin1ИСП РАНИСП РАНThe paper presents a survey of existing approaches to modeling memory states of C programs with SMT-formulas in context of static verification. The paper highlights the essential problems of C memory model development and describes two major groups of C memory models: one comprising of models that support unbounded memory regions and another including the models that don’t. Among the models for a priori bounded memory regions the paper discusses a strongest postcondition-based model relying on preliminary alias analysis and a weakest precondition-based model that uses uninterpreted functions and first-order logic to represent pointer predicates. Among the models for unbounded memory areas the paper describes a typed memory model, the Burstall-Bornat model, a region-based model and a model with full support for the Logic of Interpreted Sets and Bounded Quantification (LISBQ) earlier implemented in the HAVOC deductive verification tool.https://ispranproceedings.elpub.ru/jour/article/view/240статическая верификациямодели памятиsmt-решатели |
| spellingShingle | M. U. Mandrykin V. S. Mutilin Survey of memory modeling methods in static verification tools Труды Института системного программирования РАН статическая верификация модели памяти smt-решатели |
| title | Survey of memory modeling methods in static verification tools |
| title_full | Survey of memory modeling methods in static verification tools |
| title_fullStr | Survey of memory modeling methods in static verification tools |
| title_full_unstemmed | Survey of memory modeling methods in static verification tools |
| title_short | Survey of memory modeling methods in static verification tools |
| title_sort | survey of memory modeling methods in static verification tools |
| topic | статическая верификация модели памяти smt-решатели |
| url | https://ispranproceedings.elpub.ru/jour/article/view/240 |
| work_keys_str_mv | AT mumandrykin surveyofmemorymodelingmethodsinstaticverificationtools AT vsmutilin surveyofmemorymodelingmethodsinstaticverificationtools |