Abstracting Strings for Model Checking of C Programs

Abstracting Strings for Model Checking of C Programs

Data type abstraction plays a crucial role in software verification. In this paper, we introduce a domain for abstracting strings in the C programming language, where strings are managed as null-terminated arrays of characters. The new domain M-String is parametrized on an index (bound) domain and a...

Full description

Bibliographic Details
Main Authors: Henrich Lauko, Martina Olliaro, Agostino Cortesi, Petr Roc̆kai
Format: Article
Language:English
Published: MDPI AG 2020-11-01
Series:Applied Sciences
Subjects:
string analysis
model checking
abstract interpretation
abstract domain
Online Access:https://www.mdpi.com/2076-3417/10/21/7853

Internet

https://www.mdpi.com/2076-3417/10/21/7853

Similar Items