Software:C Bounded Model Checker
From HandWiki
Short description: 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). Jensen, Kurt; Podelski, Andreas. eds (in en). A Tool for Checking ANSI-C Programs. 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. https://link.springer.com/chapter/10.1007/978-3-540-24730-2_15.
- ↑ 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. https://ieeexplore.ieee.org/document/4544862.
- ↑
- 2020: Beyer, Dirk (2020). "Advances in Automatic Software Verification: SV-COMP 2020". in Biere, Armin; Parker, David (in en). 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. 12079. Cham: Springer International Publishing. 347–367. doi:10.1007/978-3-030-45237-7_21. ISBN 978-3-030-45237-7.
- 2021: Beyer, Dirk (2021). "Software Verification: 10th Comparative Evaluation (SV-COMP 2021)". in Groote, Jan Friso; Larsen, Kim Guldstrand (in en). 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. 12652. Cham: Springer International Publishing. 401–422. doi:10.1007/978-3-030-72013-1_24. ISBN 978-3-030-72013-1.
- 2022: Beyer, Dirk (2022). "Progress on Software Verification: SV-COMP 2022". in Fisman, Dana; Rosu, Grigore (in en). 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. 13244. Cham: Springer International Publishing. 375–402. doi:10.1007/978-3-030-99527-0_20. ISBN 978-3-030-99527-0. https://link.springer.com/chapter/10.1007/978-3-030-99527-0_20.
- ↑ Chong, Nathan; Cook, Byron; Eidelman, Jonathan; Kallas, Konstantinos; Khazem, Kareem; Monteiro, Felipe R.; Schwartz‐Narbonne, Daniel; Tasiran, Serdar et al. (April 2021). "Code‐level model checking in the software development workflow at Amazon Web Services" (in en). Software: Practice and Experience 51 (4): 772–797. doi:10.1002/spe.2949. ISSN 0038-0644. https://onlinelibrary.wiley.com/doi/10.1002/spe.2949.
- ↑ Cook, Byron; Khazem, Kareem; Kroening, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (2018). Chockler, Hana; Weissenbacher, Georg. eds (in en). Model Checking Boot Code from AWS Data Centers. 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. https://link.springer.com/chapter/10.1007/978-3-319-96142-2_28.
- ↑
- 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. https://dl.acm.org/doi/10.1145/3510457.3513031.
- 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. https://ieeexplore.ieee.org/document/7371997.
- ↑ Cordeiro, Lucas; Kesseli, Pascal; Kroening, Daniel; Schrammel, Peter; Trtik, Marek (2018). Chockler, Hana; Weissenbacher, Georg. eds (in en). JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. 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. https://link.springer.com/chapter/10.1007/978-3-319-96145-3_10.
External links
 |  |
