C Bounded Model Checker
 | This article, C Bounded Model Checker, has recently been created via the Articles for creation process. Please check to see if the reviewer has accidentally left this template after accepting the draft and take appropriate action as necessary.
Reviewer tools: Inform author |
| This article, C Bounded Model Checker, has recently been created via the Articles for creation process. Please check to see if the reviewer has accidentally left this template after accepting the draft and take appropriate action as necessary.
Reviewer tools: Inform author |
In the context of computer science, the C Bounded Model Checker (CBMC) is a bounded model checker for C programs.[1] It was the first such tool.[2]
CBMC has participated in the Competition on Software Verification (SV-COMP) in the years 2014-2022.[3] It came in first in at least one category in 2014, 2015, and 2017.
Applications
CBMC has been used to verify C code at Amazon Web Services.[4][5] It is used as model checker in the Kani and Crust verifiers for Rust,[6] and the JBMC bounded model checker for Java.[7]
References
- ^ Clarke, Edmund; Kroening, Daniel; Lerda, Flavio (2004). Jensen, Kurt; Podelski, Andreas (eds.). "A Tool for Checking ANSI-C Programs". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 168–176. doi:10.1007/978-3-540-24730-2_15. ISBN 978-3-540-24730-2.
- ^ D'Silva, Vijay; Kroening, Daniel; Weissenbacher, Georg (2008-07). "A Survey of Automated Techniques for Formal Software Verification". IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 27 (7): 1165–1178. doi:10.1109/TCAD.2008.923410. ISSN 0278-0070.
{{cite journal}}: Check date values in:|date=(help) - ^
- 2020: Beyer, Dirk (2020). Biere, Armin; Parker, David (eds.). "Advances in Automatic Software Verification: SV-COMP 2020". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 347–367. doi:10.1007/978-3-030-45237-7_21. ISBN 978-3-030-45237-7. PMC 7480704.
{{cite journal}}: CS1 maint: PMC format (link) - 2021: Beyer, Dirk (2021). Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). "Software Verification: 10th Comparative Evaluation (SV-COMP 2021)". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 401–422. doi:10.1007/978-3-030-72013-1_24. ISBN 978-3-030-72013-1. PMC 7984550.
{{cite journal}}: CS1 maint: PMC format (link) - 2022: Beyer, Dirk (2022). Fisman, Dana; Rosu, Grigore (eds.). "Progress on Software Verification: SV-COMP 2022". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 375–402. doi:10.1007/978-3-030-99527-0_20. ISBN 978-3-030-99527-0.
- 2020: Beyer, Dirk (2020). Biere, Armin; Parker, David (eds.). "Advances in Automatic Software Verification: SV-COMP 2020". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing: 347–367. doi:10.1007/978-3-030-45237-7_21. ISBN 978-3-030-45237-7. PMC 7480704.
- ^ Chong, Nathan; Cook, Byron; Eidelman, Jonathan; Kallas, Konstantinos; Khazem, Kareem; Monteiro, Felipe R.; Schwartz‐Narbonne, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (2021-04). "Code‐level model checking in the software development workflow at Amazon Web Services". Software: Practice and Experience. 51 (4): 772–797. doi:10.1002/spe.2949. ISSN 0038-0644.
{{cite journal}}: Check date values in:|date=(help) - ^ Cook, Byron; Khazem, Kareem; Kroening, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (2018). Chockler, Hana; Weissenbacher, Georg (eds.). "Model Checking Boot Code from AWS Data Centers". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 467–486. doi:10.1007/978-3-319-96142-2_28. ISBN 978-3-319-96142-2.
- ^
- For Kani: VanHattum, Alexa; Schwartz-Narbonne, Daniel; Chong, Nathan; Sampson, Adrian (2022-10-17). "Verifying dynamic trait objects in rust". Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice. ICSE-SEIP '22. New York, NY, USA: Association for Computing Machinery: 321–330. doi:10.1145/3510457.3513031. ISBN 978-1-4503-9226-6.
- For Crust: Toman, John; Pernsteiner, Stuart; Torlak, Emina (2015-11). "Crust: A Bounded Verifier for Rust (N)". IEEE: 75–80. doi:10.1109/ASE.2015.77. ISBN 978-1-5090-0025-8.
{{cite journal}}: Check date values in:|date=(help); Cite journal requires|journal=(help)
- ^ Cordeiro, Lucas; Kesseli, Pascal; Kroening, Daniel; Schrammel, Peter; Trtik, Marek (2018). Chockler, Hana; Weissenbacher, Georg (eds.). "JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 183–190. doi:10.1007/978-3-319-96145-3_10. ISBN 978-3-319-96145-3.