Domain types: abstract-domain selection based on variable usage
Conference paper
Apel, S., Beyer, D., Friedberger, K., Raimondi, F. and von Rhein, A. 2013. Domain types: abstract-domain selection based on variable usage. Bertacco, V. and Legay, A. (ed.) 9th International Haifa Verification Conference (HVC 2013). Haifa, Israel 05 - 07 Nov 2013 Springer. pp. 262-278 https://doi.org/10.1007/978-3-319-03077-7_18
| Type | Conference paper |
|---|---|
| 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. |
| Conference | 9th International Haifa Verification Conference (HVC 2013) |
| Page range | 262-278 |
| Proceedings Title | Hardware and Software: Verification and Testing: 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings |
| Series | Lecture Notes in Computer Science |
| Editors | Bertacco, V. and Legay, A. |
| ISSN | 0302-9743 |
| Electronic | 1611-3349 |
| ISBN | |
| Paperback | 9783319030760 |
| Electronic | 9783319030777 |
| Publisher | Springer |
| Publication dates | |
| 31 Oct 2013 | |
| Publication process dates | |
| Deposited | 23 Apr 2015 |
| Output status | Published |
| Digital Object Identifier (DOI) | https://doi.org/10.1007/978-3-319-03077-7_18 |
| Web address (URL) of conference proceedings | https://doi.org/10.1007/978-3-319-03077-7 |
| Language | English |
https://repository.mdx.ac.uk/item/850yy
163
total views0
total downloads2
views this month0
downloads this month