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