Verificador de modelos acotados de C

El C Bounded Model Checker ( CBMC ) es un verificador de modelos acotado para programas informáticos escritos en C. ^{[ 1 ]} Fue la primera herramienta de este tipo. ^{[ 2 ]}

CBMC ha participado en la Competencia de Verificación de Software (SV-COMP) en los años 2014–2022. ^{[ 3 ]} Quedó en primer lugar en al menos una categoría en 2014, 2015 y 2017.

Aplicaciones

CBMC se ha utilizado para verificar código C en Amazon Web Services . ^{[ 4 ]}^{[ 5 ]} Se utiliza como verificador de modelos en los verificadores Kani y Crust para Rust , ^{[ 6 ]} y el verificador de modelos acotado JBMC para Java . ^{[ 7 ]}

Referencias

↑ Clarke, Edmund; Kroening, Daniel; Lerda, Flavio (2004). «Una herramienta para comprobar programas ANSI-C» . En Jensen, Kurt; Podelski, Andreas (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Berlín, 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 (julio de 2008). "Un estudio de técnicas automatizadas para la verificación formal de software". 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 .
↑
- 2020: Beyer, Dirk (2020). «Avances en la verificación automática de software: SV-COMP 2020». En Biere, Armin; Parker, David (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 26.ª Conferencia Internacional, TACAS 2020, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2020, Dublín, Irlanda, 25-30 de abril de 2020, Actas, Parte 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=ignorado ( ayuda )
- 2021: Beyer, Dirk (2021). "Verificación de software: 10.ª Evaluación comparativa (SV-COMP 2021)". En Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 27.ª Conferencia Internacional, TACAS 2021, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2021, Ciudad de Luxemburgo, Luxemburgo, 27 de marzo - 1 de abril de 2021, Actas, Parte 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=ignorado ( ayuda )
- 2022: Beyer, Dirk (2022). "Avances en la verificación de software: SV-COMP 2022" . En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 28.ª Conferencia Internacional, TACAS 2022, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2022, Múnich, Alemania, 2-7 de abril de 2022, Actas, Parte 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=ignorado ( ayuda )
↑ Chong, Nathan; Cook, Byron; Eidelman, Jonathan; Kallas, Konstantinos; Khazem, Kareem; Monteiro, Felipe R.; Schwartz-Narbonne, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (abril de 2021). "Verificación de modelos a nivel de código en el flujo de trabajo de desarrollo de software en 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" . En 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.
↑
- Para Kani: VanHattum, Alexa; Schwartz-Narbonne, Daniel; Chong, Nathan; Sampson, Adrian (17 de octubre de 2022). "Verificación de objetos de rasgos dinámicos en Rust". Actas de la 44.ª Conferencia Internacional sobre Ingeniería de Software: Ingeniería de Software en la Práctica . ICSE-SEIP '22. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 321–330 . doi : 10.1145/3510457.3513031 . ISBN 978-1-4503-9226-6. S2CID 247148388 .
- Para Crust: Toman, John; Pernsteiner, Stuart; Torlak, Emina (noviembre de 2015). Crust: Un verificador acotado para Rust (N) . IEEE. págs. 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: Una herramienta de verificación de modelos acotada para verificar el bytecode de Java" . En Chockler, Hana; Weissenbacher, Georg (eds.). Verificación asistida por computadora . 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.

Enlaces externos

Sitio web oficial

[1] Clarke, Edmund; Kroening, Daniel; Lerda, Flavio (2004). «Una herramienta para comprobar programas ANSI-C» . En Jensen, Kurt; Podelski, Andreas (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Berlín, 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 (julio de 2008). "Un estudio de técnicas automatizadas para la verificación formal de software". 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). «Avances en la verificación automática de software: SV-COMP 2020». En Biere, Armin; Parker, David (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 26.ª Conferencia Internacional, TACAS 2020, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2020, Dublín, Irlanda, 25-30 de abril de 2020, Actas, Parte 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=ignorado ( ayuda )
2021: Beyer, Dirk (2021). "Verificación de software: 10.ª Evaluación comparativa (SV-COMP 2021)". En Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 27.ª Conferencia Internacional, TACAS 2021, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2021, Ciudad de Luxemburgo, Luxemburgo, 27 de marzo - 1 de abril de 2021, Actas, Parte 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=ignorado ( ayuda )
2022: Beyer, Dirk (2022). "Avances en la verificación de software: SV-COMP 2022" . En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 28.ª Conferencia Internacional, TACAS 2022, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2022, Múnich, Alemania, 2-7 de abril de 2022, Actas, Parte 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=ignorado ( ayuda )

[mwVQ] 2020: Beyer, Dirk (2020). «Avances en la verificación automática de software: SV-COMP 2020». En Biere, Armin; Parker, David (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 26.ª Conferencia Internacional, TACAS 2020, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2020, Dublín, Irlanda, 25-30 de abril de 2020, Actas, Parte 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=ignorado ( ayuda )

[mwbw] 2021: Beyer, Dirk (2021). "Verificación de software: 10.ª Evaluación comparativa (SV-COMP 2021)". En Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 27.ª Conferencia Internacional, TACAS 2021, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2021, Ciudad de Luxemburgo, Luxemburgo, 27 de marzo - 1 de abril de 2021, Actas, Parte 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=ignorado ( ayuda )

[mwiQ] 2022: Beyer, Dirk (2022). "Avances en la verificación de software: SV-COMP 2022" . En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas: 28.ª Conferencia Internacional, TACAS 2022, celebrada como parte de las Conferencias Conjuntas Europeas sobre Teoría y Práctica del Software, ETAPS 2022, Múnich, Alemania, 2-7 de abril de 2022, Actas, Parte 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=ignorado ( ayuda )

[4] Chong, Nathan; Cook, Byron; Eidelman, Jonathan; Kallas, Konstantinos; Khazem, Kareem; Monteiro, Felipe R.; Schwartz-Narbonne, Daniel; Tasiran, Serdar; Tautschnig, Michael; Tuttle, Mark R. (abril de 2021). "Verificación de modelos a nivel de código en el flujo de trabajo de desarrollo de software en 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" . En 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] 
Para Kani: VanHattum, Alexa; Schwartz-Narbonne, Daniel; Chong, Nathan; Sampson, Adrian (17 de octubre de 2022). "Verificación de objetos de rasgos dinámicos en Rust". Actas de la 44.ª Conferencia Internacional sobre Ingeniería de Software: Ingeniería de Software en la Práctica . ICSE-SEIP '22. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 321–330 . doi : 10.1145/3510457.3513031 . ISBN 978-1-4503-9226-6. S2CID 247148388 .
Para Crust: Toman, John; Pernsteiner, Stuart; Torlak, Emina (noviembre de 2015). Crust: Un verificador acotado para Rust (N) . IEEE. págs. 75–80 . doi : 10.1109/ASE.2015.77 . ISBN 978-1-5090-0025-8. S2CID 582915 .

[mwxQ] Para Kani: VanHattum, Alexa; Schwartz-Narbonne, Daniel; Chong, Nathan; Sampson, Adrian (17 de octubre de 2022). "Verificación de objetos de rasgos dinámicos en Rust". Actas de la 44.ª Conferencia Internacional sobre Ingeniería de Software: Ingeniería de Software en la Práctica . ICSE-SEIP '22. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 321–330 . doi : 10.1145/3510457.3513031 . ISBN 978-1-4503-9226-6. S2CID 247148388 .

[mw1Q] Para Crust: Toman, John; Pernsteiner, Stuart; Torlak, Emina (noviembre de 2015). Crust: Un verificador acotado para Rust (N) . IEEE. págs. 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: Una herramienta de verificación de modelos acotada para verificar el bytecode de Java" . En Chockler, Hana; Weissenbacher, Georg (eds.). Verificación asistida por computadora . 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 ]

Aplicaciones

Referencias

Enlaces externos

Articulos relacionados