ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO a Agostino CORTESI. String Abstraction for Model Checking of C Programs. In Fabrizio Biondi, Thomas Given-Wilson, Axel Legay. Model Checking Software. Cham: Springer International Publishing, 2019. s. 74-93. ISBN 978-3-030-30922-0. doi:10.1007/978-3-030-30923-7_5.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW URL
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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-30923-7_5
Klíčová slova anglicky Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
Štítky firank_B
Příznaky Mezinárodní význam
Změnil Změnila: Martina Olliaro, Ph.D., učo 477767. Změněno: 11. 9. 2020 09:45.
Anotace
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 VaVNázev: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Standardní projekty
MUNI/A/1018/2018, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 9. 12. 2021 15:45