LTL Model Checking of LLVM Bitcode with Symbolic Data

BAUCH, Petr, Vojtěch HAVEL and Jiří BARNAT. LTL Model Checking of LLVM Bitcode with Symbolic Data. Online. In P. Hlineny et al. Proceedings of MEMICS'14. Telc: Springer, 2014, p. 47-59. ISBN 978-3-319-14895-3. Available from: https://dx.doi.org/10.1007/978-3-319-14896-0_5.

Basic information

Original name

LTL Model Checking of LLVM Bitcode with Symbolic Data

Authors

BAUCH, Petr (203 Czech Republic, belonging to the institution), Vojtěch HAVEL (203 Czech Republic, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)

Edition

Telc, Proceedings of MEMICS'14, p. 47-59, 13 pp. 2014

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/14:00077311

Organization unit

Faculty of Informatics

ISBN

978-3-319-14895-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-14896-0_5

UT WoS

000357573300005

Keywords in English

llvm; formal verification; model checking

Tags

International impact, Reviewed

---

Abstract

V originále

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 interleavings of 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.

---

Links

MUNI/A/0765/2013, interní kód MU	Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU) Investor: Masaryk University, Category A
MUNI/A/0855/2013, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.) Investor: Masaryk University, Category A
7H13001, research and development project	Name: Critical System Engineering Acceleration (Acronym: CRYSTAL (MSMT)) Investor: Ministry of Education, Youth and Sports of the CR