Cooperating Validity Checker information

CVC5
Developer(s)	Stanford University and University of Iowa
Initial release	2022; 2 years ago
Stable release	1.0.8 / 31 August 2023
Written in	C++
Operating system	Windows, Linux, macOS
Type	Theorem prover
License	BSD 3-clause
Website	cvc5.github.io

In computer science and mathematical logic, Cooperating Validity Checker (CVC) is a family of satisfiability modulo theories (SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 (stylized cvc5); earlier versions include CVC, CVC Lite, and CVC3.^[2] Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats.^[3]^[4] cvc5 has bindings for C++, Python, and Java.

CVC4 competed in SMT-COMP in the years 2014-2020,^[5] and cvc5 has competed in the years 2021-2022.^[6] CVC4 competed in SyGuS-COMP in the years 2015-2019,^[7] and in CASC in 2013-2015.

CVC4 uses the DPLL(T) architecture,^[8] and supports the theories of linear arithmetic over rationals and integers, fixed-width bitvectors,^[9] floating-point arithmetic,^[10] strings,^[11] (co)-datatypes,^[12] sequences (used to model dynamic arrays),^[13] finite sets and relations,^[14]^[15] separation logic,^[16] and uninterpreted functions among others. cvc5 additionally supports finite fields.^[17]

In addition to standard SMT and SyGuS solving, cvc5 supports abductive reasoning, which is the problem of constructing a formula $B$ that can be conjoined with a formula $A$ to prove a goal formula $C$ .^[18]^[19]

cvc5 has been subject to several independent test campaigns.^[20]

^ "Release cvc5-1.0.8 · cvc5/cvc5". GitHub. Retrieved 2023-11-29.
^ Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), "Satisfiability Modulo Theories", 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
^ 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). "Flexible Proof Production in an Industrial-Strength SMT Solver". In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning. 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.
^ (Barbosa et al. 2022, p. 417)
^ "Participants". SMT-COMP. Retrieved 2023-11-29.
^ "SMT-COMP". SMT-COMP. Retrieved 2023-11-29.
^
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Results and Analysis of SyGuS-Comp'15". Electronic Proceedings in Theoretical Computer Science. 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 (2016-11-22). "SyGuS-Comp 2016: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 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: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 260: 97–115. arXiv:1711.11438. doi:10.4204/EPTCS.260.9. ISSN 2075-2180. S2CID 37464992.
^ 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.
^ 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.
^ Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). Dillig, Isil; Tasiran, Serdar (eds.). Invertibility Conditions for Floating-Point Formulas. 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. {{cite book}}: |journal= ignored (help)
^ 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.
^ 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.
^ Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences". Journal of Automated Reasoning. 67 (3): 32. doi:10.1007/s10817-023-09682-2. ISSN 1573-0670. S2CID 261829653.
^ Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). "A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT". In Olivetti, Nicola; Tiwari, Ashish (eds.). Automated Reasoning. 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.
^ Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "Relational Constraint Solving in SMT". In de Moura, Leonardo (ed.). Automated Deduction – 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.
^ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "A Decision Procedure for Separation Logic in SMT" (PDF). In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). Automated Technology for Verification and Analysis. 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.
^ Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "Satisfiability Modulo Finite Fields". In Enea, Constantin; Lal, Akash (eds.). Computer Aided Verification. 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.
^ Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). "Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis". Automated Reasoning. Lecture Notes in Computer Science. Vol. 12166. pp. 141–160. doi:10.1007/978-3-030-51074-9_9. ISBN 978-3-030-51073-2. PMC 7324138.
^ (Barbosa et al. 2022, p. 426)
^
- Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05). "Finding and Understanding Incompleteness Bugs in SMT Solvers". Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. ASE '22. New York, NY, USA: Association for Computing Machinery. pp. 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 (2023-07-26). "Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 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: A Modular and Highly Extensible API Fuzzer for SMT Solvers". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. 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 (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 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). "SMT Solver Validation Empowered by Large Pre-Trained Language Models". 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 1288–1300. doi:10.1109/ase56229.2023.00180. ISBN 979-8-3503-2996-4. S2CID 265055537. Retrieved 2023-11-29.
- Bringolf, Mauro (2021). Fuzz-testing SMT Solvers with Formula Weakening and Strengthening (Master Thesis thesis). ETH Zurich. doi:10.3929/ethz-b-000507582.

[1] "Release cvc5-1.0.8 · cvc5/cvc5". GitHub. Retrieved 2023-11-29.

[2] Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), "Satisfiability Modulo Theories", 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). "Flexible Proof Production in an Industrial-Strength SMT Solver". In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning. 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] "Participants". SMT-COMP. Retrieved 2023-11-29.

[6] "SMT-COMP". SMT-COMP. Retrieved 2023-11-29.

[7] 
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Results and Analysis of SyGuS-Comp'15". Electronic Proceedings in Theoretical Computer Science. 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 (2016-11-22). "SyGuS-Comp 2016: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 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: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 260: 97–115. arXiv:1711.11438. doi:10.4204/EPTCS.260.9. ISSN 2075-2180. S2CID 37464992.

[8] Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Results and Analysis of SyGuS-Comp'15". Electronic Proceedings in Theoretical Computer Science. 202: 3–26. arXiv:1602.01170. doi:10.4204/EPTCS.202.3. ISSN 2075-2180. S2CID 2086015.

[9] Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 229: 178–202. arXiv:1611.07627. doi:10.4204/EPTCS.229.13. ISSN 2075-2180. S2CID 440389.

[10] Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 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). Dillig, Isil; Tasiran, Serdar (eds.). Invertibility Conditions for Floating-Point Formulas. 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. {{cite book}}: |journal= ignored (help)

[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). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences". 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). "A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT". In Olivetti, Nicola; Tiwari, Ashish (eds.). Automated Reasoning. 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). "Relational Constraint Solving in SMT". In de Moura, Leonardo (ed.). Automated Deduction – 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). "A Decision Procedure for Separation Logic in SMT" (PDF). In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). Automated Technology for Verification and Analysis. 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). "Satisfiability Modulo Finite Fields". In Enea, Constantin; Lal, Akash (eds.). Computer Aided Verification. 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 (2020-05-30). "Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis". Automated Reasoning. Lecture Notes in Computer Science. Vol. 12166. pp. 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 (2023-01-05). "Finding and Understanding Incompleteness Bugs in SMT Solvers". Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. ASE '22. New York, NY, USA: Association for Computing Machinery. pp. 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 (2023-07-26). "Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 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: A Modular and Highly Extensible API Fuzzer for SMT Solvers". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. 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 (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 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). "SMT Solver Validation Empowered by Large Pre-Trained Language Models". 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 1288–1300. doi:10.1109/ase56229.2023.00180. ISBN 979-8-3503-2996-4. S2CID 265055537. Retrieved 2023-11-29.

Bringolf, Mauro (2021). Fuzz-testing SMT Solvers with Formula Weakening and Strengthening (Master Thesis thesis). ETH Zurich. doi:10.3929/ethz-b-000507582.

[24] Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05). "Finding and Understanding Incompleteness Bugs in SMT Solvers". Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. ASE '22. New York, NY, USA: Association for Computing Machinery. pp. 1–10. doi:10.1145/3551349.3560435. ISBN 978-1-4503-9475-8. S2CID 255441416.

[25] Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (2023-07-26). "Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 69–81. doi:10.1109/ICSE48619.2023.00018. ISBN 978-1-6654-5701-9. S2CID 259860528.

[26] Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). "Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. 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.

[27] Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations". 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 2224–2236. doi:10.1109/ICSE48619.2023.00187. ISBN 978-1-6654-5701-9. S2CID 259860926.

[28] Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023). "SMT Solver Validation Empowered by Large Pre-Trained Language Models". 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 1288–1300. doi:10.1109/ase56229.2023.00180. ISBN 979-8-3503-2996-4. S2CID 265055537. Retrieved 2023-11-29.

[29] Bringolf, Mauro (2021). Fuzz-testing SMT Solvers with Formula Weakening and Strengthening (Master Thesis thesis). ETH Zurich. doi:10.3929/ethz-b-000507582.

Cooperating Validity Checker information

and 13 Related for: Cooperating Validity Checker information

Cooperating Validity Checker

List of Nova episodes

Separation logic

Sarah Palin

Tandem Computers

2020 United States presidential election

Gamma correction

William Barr

Steele dossier

Joe Arpaio

Lie

Presidency of Donald Trump

Buddhism and violence