Journal article icon

Journal article

Scalable shape analysis for systems code

Abstract:

Pointer safety faults in device drivers are one of the leading causes of crashes in operating systems code. In principle, shape analysis tools can be used to prove the absence of this type of error. In practice, however, shape analysis is not used due to the unacceptable mixture of scalability and precision provided by existing tools. In this paper we report on a new join operation for the separation domain which aggressively abstracts information for scalability yet does not lead to false er...

Expand abstract
Publication status:
Published

Actions


Access Document


Authors


More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Berdine, J More by this author
Calcagno, C More by this author
Expand authors...
Journal:
COMPUTER AIDED VERIFICATION
Volume:
5123
Pages:
385-398
Publication date:
2008
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:11ef3a1d-441f-489c-9ea4-fc4be0f9e377
Source identifiers:
331489
Local pid:
pubs:331489
Language:
English

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP