String Abstraction for Model Checking of C Programs

D 2019

String Abstraction for Model Checking of C Programs

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

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

electronic version available online

References:

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

DOI

http://dx.doi.org/10.1007/978-3-030-30923-7_5

UT WoS

000876678900005

Keywords in English

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

Abstract

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.

Links

GA18-02177S, research and development project

Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Czech Science Foundation

MUNI/A/1018/2018, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

Investor: Masaryk University, Category A

Citovat

ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO and Agostino CORTESI. String Abstraction for Model Checking of C Programs. Online. 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. Available from: https://dx.doi.org/10.1007/978-3-030-30923-7_5.

@inproceedings{1576598,
   author = {Ročkai, Petr and Lauko, Henrich and Olliaro, Martina and Cortesi, Agostino},
   address = {Cham},
   booktitle = {Model Checking Software},
   doi = {http://dx.doi.org/10.1007/978-3-030-30923-7_5},
   editor = {Fabrizio Biondi, Thomas Given-Wilson, Axel Legay},
   keywords = {Symbolic Computation; String Abstraction; DIVINE; LLVM; Transformation; Verification; Model Checking; C; C++},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-30922-0},
   pages = {74-93},
   publisher = {Springer International Publishing},
   title = {String Abstraction for Model Checking of C Programs},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-30923-7_5},
   year = {2019}
}

TY  - JOUR
ID  - 1576598
AU  - Ročkai, Petr - Lauko, Henrich - Olliaro, Martina - Cortesi, Agostino
PY  - 2019
TI  - String Abstraction for Model Checking of C Programs
PB  - Springer International Publishing
CY  - Cham
SN  - 9783030309220
KW  - Symbolic Computation
KW  - String Abstraction
KW  - DIVINE
KW  - LLVM
KW  - Transformation
KW  - Verification
KW  - Model Checking
KW  - C
KW  - C++
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-30923-7_5
L2  - https://link.springer.com/chapter/10.1007%2F978-3-030-30923-7_5
N2  - 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.
ER  -

ROČKAI, Petr, Henrich LAUKO, Martina OLLIARO and Agostino CORTESI. String Abstraction for Model Checking of C Programs. Online. In Fabrizio Biondi, Thomas Given-Wilson, Axel Legay. \textit{Model Checking Software}. Cham: Springer International Publishing, 2019, p.~74-93. ISBN~978-3-030-30922-0. Available from: https://dx.doi.org/10.1007/978-3-030-30923-7\_{}5.

Detailed Information on Publication Record