Hispanopedia Wiki
Articulo de referencia

Verificador de validez cooperativo

{{Cite web |title=Release cvc5-1.2.1 · cvc5/cvc5 |url=https://github.com/cvc5/cvc5/releases/tag/cvc5-1.2.1 |access-date=2025-02-12 |website=GitHub |language=en}} "},"latest rele...

Hispanopedia WikiContenido en espanolLectura gratuita

En ciencias de la computación y lógica matemática , Cooperating Validity Checker (CVC) es una familia de solucionadores de satisfacibilidad módulo teorías (SMT). Las últimas versiones principales de CVC son CVC4 y CVC5 (estilizado cvc5); las versiones anteriores incluyen CVC, CVC Lite y CVC3. [ 2 ] Tanto CVC4 como cvc5 admiten los formatos de entrada SMT-LIB y TPTP para resolver problemas SMT, y el formato SyGuS-IF para la síntesis de programas . Tanto CVC4 como cvc5 pueden generar pruebas que pueden verificarse de forma independiente en el formato LFSC, cvc5 además admite los formatos Alethe y Lean 4. [ 3 ] [ 4 ] cvc5 tiene enlaces para C++ , Python y Java .

CVC4 compitió en SMT-COMP en los años 2014-2020, [ 5 ] y cvc5 compitió en los años 2021-2022. [ 6 ] CVC4 compitió en SyGuS-COMP en los años 2015-2019, [ 7 ] y en CASC en 2013-2015.

CVC4 utiliza la arquitectura DPLL(T) , [ 8 ] y admite las teorías de aritmética lineal sobre racionales y enteros , vectores de bits de ancho fijo, [ 9 ] aritmética de punto flotante , [ 10 ] cadenas , [ 11 ] (co)tipos de datos , [ 12 ] secuencias (utilizadas para modelar matrices dinámicas ), [ 13 ] conjuntos y relaciones finitos , [ 14 ] [ 15 ] lógica de separación , [ 16 ] y funciones no interpretadas, entre otras. cvc5 admite además campos finitos . [ 17 ]

Además de la resolución estándar de SMT y SyGuS, cvc5 admite el razonamiento abductivo , que es el problema de construir una fórmula B que se pueda combinar con una fórmula A para demostrar una fórmula objetivo C. [ 18 ] [ 19 ]

cvc5 ha sido objeto de varias campañas de pruebas independientes. [ 20 ]

Aplicaciones

CVC4 se ha aplicado a la síntesis de programas recursivos [ 21 ] y a la verificación de políticas de acceso de Amazon Web Services [ 22 ] [ 23 ] . CVC4 y cvc5 se han integrado con Rocq [ 24 ] e Isabelle [ 25 ] . CVC4 es uno de los razonadores de back-end compatibles con CBMC, el C Bounded Model Checker [ 26 ] .

Referencias

  1. ↑ "Versión cvc5-1.2.1 · cvc5/cvc5" . GitHub . Consultado el 12 de febrero de 2025 .
  2. ↑ Barrett, Clark; Tinelli, Cesare (2018), "Satisfiability Modulo Theories", en Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), Handbook of Model Checking , Cham: Springer International Publishing, pp. 305–343 , doi : 10.1007/978-3-319-10575-8_11 , ISBN  978-3-319-10575-8
  3. ↑ Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022). "Producción flexible de pruebas en un solucionador SMT de nivel industrial" . En Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Razonamiento automatizado . Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35 . doi : 10.1007/978-3-031-10769-6_3 . ISBN   978-3-031-10769-6. S2CID 250164402 . 
  4. ↑ ( Barbosa et al. 2022 , p. 417) 
  5. ↑ "Participantes" . SMT-COMP . Consultado el 29/11/2023 .
  6. ↑ "SMT-COMP" . SMT-COMP . Consultado el 29/11/2023 .
  7. ↑
    • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Resultados y análisis de SyGuS-Comp'15". Actas electrónicas en ciencias de la computación teórica . 202 : 3–26 . arXiv : 1602.01170 . doi : 10.4204/EPTCS.202.3 . ISSN 2075-2180 . S2CID 2086015 .  
    • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (22 de noviembre de 2016). "SyGuS-Comp 2016: Resultados y análisis". Actas electrónicas en ciencias de la computación teórica . 229 : 178–202 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.229.13 . ISSN 2075-2180 . S2CID 440389 .  
    • Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Resultados y análisis". Actas electrónicas en ciencias de la computación teórica . 260 : 97–115 . arXiv : 1711.11438 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180 . S2CID 37464992 .  
  8. ↑Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 646–662. doi:10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9.
  9. ↑Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 680–695. doi:10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
  10. ↑Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). "Invertibility Conditions for Floating-Point Formulas". In Dillig, Isil; Tasiran, Serdar (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 116–136. doi:10.1007/978-3-030-25543-5_8. ISBN 978-3-030-25543-5.
  11. ↑Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). "A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings". In Lutz, Carsten; Ranise, Silvio (eds.). Frontiers of Combining Systems. Lecture Notes in Computer Science. Vol. 9322. Cham: Springer International Publishing. pp. 135–150. doi:10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0.
  12. ↑Reynolds, Andrew; Blanchette, Jasmin Christian (2015). "A Decision Procedure for (Co)datatypes in SMT Solvers". In Felty, Amy P.; Middeldorp, Aart (eds.). Automated Deduction - CADE-25. Lecture Notes in Computer Science. Vol. 9195. Cham: Springer International Publishing. pp. 197–213. doi:10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
  13. ↑ Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, ​​Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15). "Razonamiento sobre vectores: satisfacibilidad módulo una teoría de secuencias" . Journal of Automated Reasoning . 67 (3): 32. doi : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .  
  14. ↑ Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). "Un nuevo procedimiento de decisión para conjuntos finitos y restricciones de cardinalidad en SMT" . En Olivetti, Nicola; Tiwari, Ashish (eds.). Razonamiento automatizado . Lecture Notes in Computer Science. Vol. 9706. Cham: Springer International Publishing. pp. 82–98 . doi : 10.1007/978-3-319-40229-1_7 . ISBN   978-3-319-40229-1.
  15. ↑ Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "Resolución de restricciones relacionales en SMT" . En de Moura, Leonardo (ed.). Deducción automatizada – CADE 26. Lecture Notes in Computer Science. Vol. 10395. Cham: Springer International Publishing. pp. 148–165 . doi : 10.1007/978-3-319-63046-5_10 . ISBN   978-3-319-63046-5.
  16. ↑ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "Un procedimiento de decisión para la lógica de separación en SMT" . En Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). Tecnología automatizada para verificación y análisis . Lecture Notes in Computer Science. Vol. 9938. Cham: Springer International Publishing. pp. 244–261 . doi : 10.1007/978-3-319-46520-3_16 . ISBN   978-3-319-46520-3. S2CID 6753369 . 
  17. ↑ Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "Satisfacibilidad módulo campos finitos" . En Enea, Constantin; Lal, Akash (eds.). Verificación asistida por computadora . Lecture Notes in Computer Science. Vol. 13965. Cham: Springer Nature Switzerland. pp. 163–186 . doi : 10.1007/978-3-031-37703-7_8 . ISBN   978-3-031-37703-7. S2CID 257235627 . 
  18. ↑ Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (30 de mayo de 2020). «Algoritmos escalables para la abducción mediante síntesis guiada por sintaxis enumerativa». Razonamiento automatizado . Notas de clase en informática. Vol. 12166. págs. 141–160 . doi : 10.1007/978-3-030-51074-9_9 . ISBN   978-3-030-51073-2. PMC 7324138 . 
  19. ↑ ( Barbosa et al. 2022 , p. 426) 
  20. ↑
    • Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (5 de enero de 2023). «Detección y comprensión de errores de incompletitud en solucionadores SMT» . Actas de la 37.ª Conferencia Internacional IEEE/ACM sobre Ingeniería de Software Automatizada . ASE '22. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 1-10 . doi : 10.1145/3551349.3560435 . ISBN  978-1-4503-9475-8. S2CID 255441416 . 
    • Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (26 de julio de 2023). "Validación de solucionadores SMT mediante enumeración de esqueletos potenciada por entradas históricas que activan errores" . 45.ª Conferencia Internacional IEEE/ACM sobre Ingeniería de Software (ICSE) de 2023. ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 69–81 . doi : 10.1109/ICSE48619.2023.00018 . ISBN  978-1-6654-5701-9. S2CID 259860528 . 
    • Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). «Murxla: Un fuzzer API modular y altamente extensible para solucionadores SMT» . En Shoham, Sharon; Vizel, Yakir (eds.). Verificación asistida por computadora . Lecture Notes in Computer Science. Vol.  13372. Cham: Springer International Publishing. pp. 92–106 . doi : 10.1007/978-3-031-13188-2_5 . ISBN  978-3-031-13188-2. S2CID 251447764 . 
    • Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (26 de julio de 2023). «Diver: Pruebas de solucionadores SMT guiadas por oráculo con mutaciones aleatorias sin restricciones» . 45.ª Conferencia Internacional IEEE/ACM sobre Ingeniería de Software (ICSE) de 2023. ICSE '23. Melbourne, Victoria, Australia: IEEE Press. págs. 2224–2236 . doi : 10.1109/ICSE48619.2023.00187 . ISBN  978-1-6654-5701-9. S2CID 259860926 . 
    • Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023). "Validación de solucionadores SMT potenciada por grandes modelos de lenguaje preentrenados". 38.ª Conferencia Internacional IEEE/ACM sobre Ingeniería de Software Automatizada (ASE) de 2023. pp. 1288–1300 . doi : 10.1109/ase56229.2023.00180 . ISBN  979-8-3503-2996-4. S2CID 265055537 . 
    • Bringolf, Mauro (2021). Pruebas de fuzzing de solucionadores SMT con debilitamiento y fortalecimiento de fórmulas (tesis de maestría). ETH Zurich. doi : 10.3929/ethz-b-000507582 .
  21. ↑ Berman, Shmuel (17 de octubre de 2021). «Programación por ejemplo: Síntesis de programas en bucle» . Actas complementarias de la Conferencia Internacional ACM SIGPLAN 2021 sobre Sistemas, Programación, Lenguajes y Aplicaciones: Software para la Humanidad . SPLASH Companion 2021. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 19-21 . arXiv : 2108.08724 . doi : 10.1145/3484271.3484977 . ISBN  978-1-4503-9088-0. S2CID 237213485 . 
  22. ↑ Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (octubre de 2018). Razonamiento automatizado basado en semántica para políticas de acceso de AWS mediante SMT . IEEE. págs. 1–9 . doi : 10.23919/FMCAD.2018.8602994 . ISBN  978-0-9835678-8-2. S2CID 52237693 . 
  23. ↑ Rungta, Neha (2022). "Mil millones de consultas SMT al día (Artículo invitado)" . En Shoham, Sharon; Vizel, Yakir (eds.). Verificación asistida por computadora . Lecture Notes in Computer Science. Vol. 13371. Cham: Springer International Publishing. pp. 3–18 . doi : 10.1007/978-3-031-13185-1_1 . ISBN   978-3-031-13185-1. S2CID 251447649 . 
  24. ↑
    • Para CVC4: Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). "SMTCoq: Un complemento para integrar solucionadores SMT en Coq" (PDF) . En Majumdar, Rupak; Kunčak, Viktor (eds.). Verificación asistida por computadora . Lecture Notes in Computer Science. Vol. 10427. Cham: Springer International Publishing. pp. 126–133 . doi : 10.1007/978-3-319-63390-9_7 . ISBN   978-3-319-63390-9. S2CID 206701576 . 
    • Para cvc5: ( Barbosa et al. 2022 , p. 425) 
    • Para cvc5: Barbosa, Haniel; Keller, Chantal; Reynolds, Andrew; Viswanathan, Arjun; Tinelli, Cesare; Barrett, Clark (2023-06-03). "Una táctica SMT interactiva en Coq usando razonamiento abductivo" . EPiC Series in Computing . 94. EasyChair: 11–22 . doi : 10.29007/432m . S2CID 259070258 . 
  25. ^ Desharnais, Martín; Vukmirović, Petar; Blanchette, jazmín; Wenzel, Makarius (2022). "Diecisiete probadores bajo el martillo" . DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8 . Procedimientos internacionales de informática de Leibniz (LIPIcs). 237 . Schloss-Dagstuhl - Leibniz Zentrum für Informatik: 8:1–8:18. doi : 10.4230/LIPIcs.ITP.2022.8 . ISBN 978-3-95977-252-5. S2CID 251322787 . 
  26. ↑ Kroening, Daniel; Tautschnig, Michael (2014). "CBMC – C Bounded Model Checker" . En Ábrahám, Erika; Havelund, Klaus (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Vol. 8413. Berlín, Heidelberg: Springer. pp. 389–391 . doi : 10.1007/978-3-642-54862-8_26 . ISBN   978-3-642-54862-8.
  • Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). "Cvc5: Un solucionador SMT versátil y de nivel industrial" . En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Vol.  13243. Cham: Springer International Publishing. pp. 415–442 . doi : 10.1007/978-3-030-99524-9_24 . ISBN  978-3-030-99524-9. S2CID 247857361 . 
  • Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011). "CVC4" . En Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). Verificación asistida por computadora . Lecture Notes in Computer Science. Vol.  6806. Berlín, Heidelberg: Springer. pp. 171–177 . doi : 10.1007/978-3-642-22110-1_14 . ISBN  978-3-642-22110-1.
Obtenido de " https://en.wikipedia.org/w/index.php?title=Cooperating_Validity_Checker&oldid=1360636694 "