|
This article is cited in 1 scientific paper (total in 1 paper)
Fast and safe concrete code execution for reinforcing static analysis and verification
M. Belyaev, V. Itsykson Peter the Great St. Petersburg Polytechnic University,
Polytechnicheskaya street, 21, Saint-Petersburg, 194021, Russia
Abstract:
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.
Keywords:
concrete interpretation, symbolic execution, static code analysis, analysis precision.
Received: 15.09.2015
Citation:
M. Belyaev, V. Itsykson, “Fast and safe concrete code execution for reinforcing static analysis and verification”, Model. Anal. Inform. Sist., 22:6 (2015), 763–772
Linking options:
https://www.mathnet.ru/eng/mais472 https://www.mathnet.ru/eng/mais/v22/i6/p763
|
Statistics & downloads: |
Abstract page: | 256 | Full-text PDF : | 89 | References: | 47 |
|