2019
String Abstraction for Model Checking of C Programs
ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO a Agostino CORTESIZákladní údaje
Originální název
String Abstraction for Model Checking of C Programs
Autoři
ROČKAI, Petr (703 Slovensko, domácí), Henrich LAUKO (703 Slovensko, garant, domácí), Martina OLLIARO (380 Itálie, domácí) a Agostino CORTESI (380 Itálie)
Vydání
Cham, Model Checking Software, od s. 74-93, 20 s. 2019
Nakladatel
Springer International Publishing
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Švýcarsko
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
elektronická verze "online"
Odkazy
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/19:00107758
Organizační jednotka
Fakulta informatiky
ISBN
978-3-030-30922-0
ISSN
UT WoS
000876678900005
Klíčová slova anglicky
Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
Štítky
Příznaky
Mezinárodní význam
Změněno: 13. 5. 2024 16:24, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
Automatic abstraction is a powerful software verification technique. In this paper, we elaborate an abstract domain for C strings, that is, null-terminated arrays of characters. We describe the abstract semantics of basic string operations and prove their soundness with regards to previously established concrete semantics of those operations. In addition to a selection of string functions from the standard C library, we provide semantics for character access and update, enabling automatic lifting of arbitrary string-manipulating code into the domain. The domain we present (called M-String) has two other abstract domains as its parameters: an index (bound) domain and a character domain. Picking different constituent domains allows M-String to be tailored for specific verification tasks, balancing precision against complexity. In addition to describing the domain theoretically, we also provide an executable implementation of the abstract operations. Using a tool which automatically lifts existing programs into the M-String domain along with an explicit-state model checker, we have evaluated the proposed domain experimentally on a few simple but realistic test programs.
Návaznosti
GA18-02177S, projekt VaV |
| ||
MUNI/A/1018/2018, interní kód MU |
|