LTL Model Checking of LLVM Bitcode with Symbolic Data

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F14%3A00077311" target="_blank" >RIV/00216224:14330/14:00077311 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-14896-0_5" target="_blank" >http://dx.doi.org/10.1007/978-3-319-14896-0_5</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-14896-0_5" target="_blank" >10.1007/978-3-319-14896-0_5</a>

Result language
angličtina
Original language name
LTL Model Checking of LLVM Bitcode with Symbolic Data
Original language description
The correctness of parallel and reactive programs is often easier specified using formulae of temporal logics. Yet verifying that a system satisfies such specifications is more difficult than verifying safety properties: the recurrence of a specific program state has to be detected. This paper reports on the development of a generic framework for automatic verification of linear temporal logic specifications for programs in LLVM bitcode. Our method searches explicitly through all possible interleavingsof parallel threads (control non-determinism) but represents symbolically the variable evaluations (data non-determinism), guided by the specification in order to prove the correctness. To evaluate the framework we compare our method with state-of-the-art tools on a set of unmodified C programs.
Czech name
—
Czech description
—

Project
<a href="/en/project/7H13001" target="_blank" >7H13001: Critical System Engineering Acceleration</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2014
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)