C Bounded Model Checker

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). "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.
^ 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. doi:10.1109/TCAD.2008.923410. ISSN 0278-0070. S2CID 8921624.
^
- 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)
^ 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.
^ 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.
^
- 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.
^ 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.

External links

Official website

[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. 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] 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)

[5] 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)

[6] 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.

[10] 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.

[11] 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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]