Conference item icon

Conference item

CBMC – C bounded model checker

Abstract:

CBMC implements bit-precise bounded model checking for C programs and has been developed and maintained for more than ten years. CBMC verifies the absence of violated assertions under a given loop unwinding bound. Other properties, such as SV-COMP’s ERROR labels or memory safety properties are reduced to assertions via automated instrumentation. Only recently support for efficiently checking concurrent programs, including support for weak memory models, has been added. Thus, CBMC is now capab...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
  • (Accepted manuscript, pdf, 144.2KB)
Publisher copy:
10.1007/978-3-642-54862-8_26

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author

Contributors

Role:
Editor
Role:
Editor
Publisher:
Springer
Host title:
Lecture Notes in Computer Science: TACAS 2014: Tools and Algorithms for the Construction and Analysis of Systems
Journal:
Lecture Notes in Computer Science: TACAS 2014: Tools and Algorithms for the Construction and Analysis of Systems More from this journal
Volume:
8413
Pages:
389-391
Publication date:
2014-01-01
DOI:
ISSN:
0302-9743 and 1611-3349
ISBN:
9783642548611
Keywords:
Pubs id:
pubs:466836
UUID:
uuid:8abd5953-a942-4d54-9b63-6e062e36b62a
Local pid:
pubs:466836
Source identifiers:
466836
Deposit date:
2017-01-28

Terms of use


Views and Downloads






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

TO TOP