D 2019

String Abstraction for Model Checking of C Programs

ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO a Agostino CORTESI

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

DOI

UT WoS

000876678900005

Klíčová slova anglicky

Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++

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
Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů
MUNI/A/1018/2018, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty