ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO and 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. p. 74-93. ISBN 978-3-030-30922-0. doi:10.1007/978-3-030-30923-7_5.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name String Abstraction for Model Checking of C Programs
Authors ROČKAI, Petr (703 Slovakia, belonging to the institution), Henrich LAUKO (703 Slovakia, guarantor, belonging to the institution), Martina OLLIARO (380 Italy, belonging to the institution) and Agostino CORTESI (380 Italy).
Edition Cham, Model Checking Software, p. 74-93, 20 pp. 2019.
Publisher Springer International Publishing
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/19:00107758
Organization unit Faculty of Informatics
ISBN 978-3-030-30922-0
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-30923-7_5
Keywords in English Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++
Tags firank_B
Tags International impact
Changed by Changed by: Martina Olliaro, Ph.D., učo 477767. Changed: 11/9/2020 09:45.
Abstract
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.
Links
GA18-02177S, research and development projectName: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Czech Science Foundation, Standard Projects
MUNI/A/1018/2018, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 17/1/2022 02:27