Domain types: abstract-domain selection based on variable usage
Article
Apel, S., Beyer, D., Friedberger, K., Raimondi, F. and von Rhein, A. 2013. Domain types: abstract-domain selection based on variable usage. Hardware and Software: Verification and Testing. 8244 (1), pp. 262-278. https://doi.org/10.1007/978-3-319-03077-7_18
Type | Article |
---|---|
Title | Domain types: abstract-domain selection based on variable usage |
Authors | Apel, S., Beyer, D., Friedberger, K., Raimondi, F. and von Rhein, A. |
Abstract | The success of software model checking depends on finding an appropriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., ‘int’ and ‘long’) to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the usage of variables in the program, and then assigns each variable to an abstract domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision. |
Publisher | Springer International Publishing |
Journal | Hardware and Software: Verification and Testing |
ISSN | 0302-9743 |
Publication dates | |
05 Nov 2013 | |
Publication process dates | |
Deposited | 23 Apr 2015 |
Output status | Published |
Additional information | Series Title: Programming and Software Engineering |
Digital Object Identifier (DOI) | https://doi.org/10.1007/978-3-319-03077-7_18 |
Language | English |
Book title | Hardware and Software: Verification and Testing |
https://repository.mdx.ac.uk/item/850yy
42
total views0
total downloads1
views this month0
downloads this month