You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: Imperial College London » Outputs » Detail

Output details

11 - Computer Science and Informatics

Imperial College London

Return to search Previous output Next output

Output 39 of 201 in the submission

Article title

Automatic analysis of DMA races using model checking and k-induction

Type

D - Journal article

DOI

10.1007/s10703-011-0124-2

Title of journal

Formal Methods in System Design

Article number

Volume number

Issue number

First page of article

ISSN of journal

0925-9856

Year of publication

2011

URL

Number of additional authors

Additional information

<09> Presents an automatic analysis technique for detecting, or proving absence, of direct memory access (DMA) races in multicore software, extending a paper presented at TACAS'10 (acceptance rate 24%/110). Marks the first application of the k-induction method to software verification. The techniques have been implemented as an open source tool, SCRATCH, for analysis of programs written for the Cell BE processor. SCRATCH was used to discover a previously unknown bug in sample software for the Cell processor provided by IBM (bug report confirmed by IBM available at http://www.ibm.com/developerworks/forums/thread.jspa?messageID=14299052). Led to follow-up work on k-induction for general software verification (SAS'11).

Interdisciplinary

Cross-referral requested

Research group

E - Programming Languages and Systems

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract