LTL Model Checking of LLVM Bitcode with Symbolic Data

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

LTL Model Checking of LLVM Bitcode with Symbolic Data

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

LTL Model Checking of LLVM Bitcode with Symbolic Data

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/7H13001" target="_blank" >7H13001: Critical System Engineering Acceleration</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2014

Kód důvěrnosti údajů

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

Název statě ve sborníku

Proceedings of MEMICS'14

ISBN

9783319148953

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

13

Strana od-do

47-59

Název nakladatele

Springer

Místo vydání

Telc

Místo konání akce

Telc

Datum konání akce

1. 1. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—