협력 유효성 검사기

Cooperating Validity Checker
CVC5
개발자스탠퍼드 대학교와 아이오와 대학교
최초출시2022; 1년 전 (2022)
안정적인 방출
1.0.8[1] / 2023년 8월 31일
작성자C++
운영체제윈도우, 리눅스, macOS
유형정리 속담
면허증.BSD 3-clause
웹사이트cvc5.github.io

컴퓨터 과학과 수학 논리학에서 협력 유효성 검사(CVC)는 만족도 모듈로 이론(SMT) 해결사의 계열입니다. CVC의 최신 주요 버전은 CVC4 및 CVC5(stylized cvc5)이며, 이전 버전에는 CVC, CVC Lite 및 CVC3가 포함됩니다.[2] CVC4와 cvc5는 모두 SMT 문제 해결을 위한 SMT-LIB 및 TPTP 입력 형식과 프로그램 합성을 위한 SyGuS-IF 형식을 지원합니다. CVC4와 cvc5는 모두 독립적으로 LFSC 형식으로 확인할 수 있는 증명을 출력할 수 있으며, cvc5는 추가적으로 알레테 및 린 4 형식을 지원합니다.[3][4] cvc5는 C++, Python 및 Java에 대한 바인딩을 가지고 있습니다.

CVC4는 2014-2020년에 SMT-COMP에 참가했고,[5] CVC5는 2021-2022년에 참가했습니다.[6] CVC4는 2015-2019년 SyGuS-COMP에서,[7] 2013-2015년 CASC에서 경쟁했습니다.

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는 유한 필드를 추가로 지원합니다.[17]

cvc5는 표준 SMT 및 SyGuS 해결 외에도 목표 공식 C를 증명하기 위해 공식 A와 결합할 수 있는 공식 B를 구성하는 문제인 납북 추론을 지원합니다.[18][19]

cvc5는 여러 독립적인 테스트 캠페인의 대상이 되었습니다.[20]

적용들

참고 항목: 만족도 모듈로 이론 § 응용 프로그램

CVC4는 재귀적 프로그램의 합성에 적용되었습니다.[21] 그리고 아마존 웹 서비스 액세스 정책을 확인합니다.[22][23] CVC4와 CVC5는 Coq와[24] Isabelle과 통합되었습니다.[25] CVC4는 CBMC가 지원하는 백엔드 추론기 중 하나인 C 경계 모델 검사기입니다.[26]

참고문헌

  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, retrieved 2023-11-29
  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, 페이지 417)
  5. ^ "Participants". SMT-COMP. Retrieved 2023-11-29.
  6. ^ "SMT-COMP". SMT-COMP. Retrieved 2023-11-29.
  7. ^
  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". Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing: 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). "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, 페이지 426)
  20. ^
  21. ^ Berman, Shmuel (2021-10-17). "Programming-by-example by programming-by-example: Synthesis of looping programs". Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity. SPLASH Companion 2021. New York, NY, USA: Association for Computing Machinery. pp. 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 (October 2018). Semantic-based Automated Reasoning for AWS Access Policies using SMT. IEEE. pp. 1–9. doi:10.23919/FMCAD.2018.8602994. ISBN 978-0-9835678-8-2. S2CID 52237693.
  23. ^ Rungta, Neha (2022). "A Billion SMT Queries a Day (Invited Paper)". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. 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. ^
    • CVC4의 경우:
    • cvc5의 경우: (Barbosa et al. 2022, 페이지 425)
    • cvc5의 경우:
  25. ^ Desharnais, Martin; Vukmirović, Petar; Blanchette, Jasmin; Wenzel, Makarius (2022). "Seventeen Provers Under the Hammer". DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8. Schloss-Dagstuhl - Leibniz Zentrum für Informatik. doi:10.4230/LIPIcs.ITP.2022.8. S2CID 251322787.
  26. ^ Kroening, Daniel; Tautschnig, Michael (2014). "CBMC – C Bounded Model Checker". In Ábrahám, Erika; Havelund, Klaus (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 8413. Berlin, 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: A Versatile and Industrial-Strength SMT Solver". In Fisman, Dana; Rosu, Grigore (eds.). Tools and Algorithms for the Construction and Analysis of Systems. 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". In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 171–177. doi:10.1007/978-3-642-22110-1_14. ISBN 978-3-642-22110-1.