Output details
11 - Computer Science and Informatics
University of Oxford
Article title
Automatic analysis of DMA races using model checking and k-induction
Type
D - Journal article
Title of journal
Formal Methods in System Design
Article number
-
Volume number
39
Issue number
1
First page of article
83
ISSN of journal
0925-9856
Year of publication
2011
Number of additional authors
2
Additional information
<07>
This paper uses k-induction, previously applied only to hardware, to verify assertions in sequential software. Intuitively, k-induction succeeds on those assertions that can be proven with a bounded amount of history, which is frequently the case for many kinds of low-level software. Our experiments on software controlling DMA for heterogeneous multicore processors demonstrate orders of magnitude speedup compared to existing methods, and reveal a bug in IBM's reference code for the Cell processor, confirmed by IBM. See http://preview.tinyurl.com/kroeningibm
This paper is an extension of our TACAS 2010 paper, and the tool described was also presented at PPOPP 2011.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
6
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
