Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification
| Autor: | M. Belyaev, V. Itsykson |
|---|---|
| Jazyk: | English<br />Russian |
| Rok vydání: | 2015 |
| Předmět: | |
| Zdroj: | Моделирование и анализ информационных систем, Vol 22, Iss 6, Pp 763-772 (2015) |
| Druh dokumentu: | article |
| ISSN: | 1818-1015 2313-5417 |
| DOI: | 10.18255/1818-1015-2015-6-763-772 |
| Popis: | The problem of improving precision of static analysis and verification techniques for C is hard due to simplification assumptions these techniques make about the code model. We present a novel approach to improving precision by executing the code model in a controlled environment that captures program errors and contract violations in a memory and time efficient way. We implemented this approach as an executor module Tassadar as a part of bounded model checker Borealis. We tested Tassadar on two test sets, showing that its impact on performance of Borealis is minimal.The article is published in the authors’ wording. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|