C Bounded Model Checker

Last updated
C Bounded Model Checker
Website www.cprover.org/cbmc/

The C Bounded Model Checker (CBMC) is a bounded model checker for computer programs written in C. [1] It was the first such tool. [2]

Contents

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

  1. ↑ Clarke, Edmund; Kroening, Daniel; Lerda, Flavio (2004). "A Tool for Checking ANSI-C Programs". In Jensen, Kurt; Podelski, Andreas (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. pp. 168–176. doi:10.1007/978-3-540-24730-2_15. ISBN   978-3-540-24730-2.
  2. ↑ D'Silva, Vijay; Kroening, Daniel; Weissenbacher, Georg (July 2008). "A Survey of Automated Techniques for Formal Software Verification". IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 27 (7): 1165–1178. Bibcode:2008ITCAD..27.1165D. doi:10.1109/TCAD.2008.923410. ISSN   0278-0070. S2CID   8921624.
  3. ↑
    • 2020: Beyer, Dirk (2020). "Advances in Automatic Software Verification: SV-COMP 2020". In Biere, Armin; Parker, David (eds.). Tools and Algorithms for the Construction and Analysis of Systems: 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part II. Lecture Notes in Computer Science. Vol. 12079. Cham: Springer International Publishing. pp. 347–367. doi:10.1007/978-3-030-45237-7_21. ISBN   978-3-030-45237-7. PMC   7480704 .{{cite book}}: |journal= ignored (help)
    • 2021: Beyer, Dirk (2021). "Software Verification: 10th Comparative Evaluation (SV-COMP 2021)". In Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science. Vol. 12652. Cham: Springer International Publishing. pp. 401–422. doi:10.1007/978-3-030-72013-1_24. ISBN   978-3-030-72013-1. PMC   7984550 .{{cite book}}: |journal= ignored (help)
    • 2022: Beyer, Dirk (2022). "Progress on Software Verification: SV-COMP 2022". In Fisman, Dana; Rosu, Grigore (eds.). Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. Lecture Notes in Computer Science. Vol. 13244. Cham: Springer International Publishing. pp. 375–402. doi:10.1007/978-3-030-99527-0_20. ISBN   978-3-030-99527-0.{{cite book}}: |journal= ignored (help)
  4. ↑ Chong, Nathan; Cook, Byron; Eidelman, Jonathan; Kallas, Konstantinos; Khazem, Kareem; Monteiro, Felipe R.; Schwartz-Narbonne, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (April 2021). "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. S2CID   232125039.
  5. ↑ Cook, Byron; Khazem, Kareem; Kroening, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (2018). "Model Checking Boot Code from AWS Data Centers". In Chockler, Hana; Weissenbacher, Georg (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 467–486. doi:10.1007/978-3-319-96142-2_28. ISBN   978-3-319-96142-2.
  6. ↑
    • 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. pp. 321–330. doi: 10.1145/3510457.3513031 . ISBN   978-1-4503-9226-6. S2CID   247148388.
    • For Crust: Toman, John; Pernsteiner, Stuart; Torlak, Emina (November 2015). Crust: A Bounded Verifier for Rust (N). IEEE. pp. 75–80. doi:10.1109/ASE.2015.77. ISBN   978-1-5090-0025-8. S2CID   582915.
  7. ↑ Cordeiro, Lucas; Kesseli, Pascal; Kroening, Daniel; Schrammel, Peter; Trtik, Marek (2018). "JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode". In Chockler, Hana; Weissenbacher, Georg (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 183–190. doi:10.1007/978-3-319-96145-3_10. ISBN   978-3-319-96145-3.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.