{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T18:17:05Z","timestamp":1773512225485,"version":"3.50.1"},"publisher-location":"Cham","reference-count":138,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:sc>cvc5<\/jats:sc> is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of <jats:sc>cvc5<\/jats:sc> \u2019s architectural design and highlights the major features and components introduced since CVC4 \u00a01.8. We evaluate <jats:sc>cvc5<\/jats:sc> \u2019s performance on all benchmarks in SMT-LIB and provide a comparison against CVC4 and Z3.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_24","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"415-442","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":340,"title":["cvc5: A Versatile and Industrial-Strength SMT Solver"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4216-7151","authenticated-orcid":false,"given":"Martin","family":"Brain","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0393-5739","authenticated-orcid":false,"given":"Gereon","family":"Kremer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3355-7828","authenticated-orcid":false,"given":"Hanna","family":"Lachnitt","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1555-5784","authenticated-orcid":false,"given":"Makai","family":"Mann","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1414-7073","authenticated-orcid":false,"given":"Abdalrhman","family":"Mohamed","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4644-5756","authenticated-orcid":false,"given":"Mudathir","family":"Mohamed","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8669-0011","authenticated-orcid":false,"given":"Andres","family":"N\u00f6tzli","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0181-6752","authenticated-orcid":false,"given":"Alex","family":"Ozdemir","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1883-2126","authenticated-orcid":false,"given":"Ying","family":"Sheng","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1brah\u00e1m, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program. 119, 100633 (2021). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100633","DOI":"10.1016\/j.jlamp.2020.100633"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp.\u00a01\u20138. IEEE (2013), https:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp.\u00a01\u20138. IEEE (2013), http:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"24_CR4","doi-asserted-by":"publisher","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 319\u2013336 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_18","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"24_CR5","doi-asserted-by":"publisher","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A\u00a0modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs. Lecture Notes in Computer Science, vol.\u00a07086, pp. 135\u2013150. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"24_CR6","unstructured":"cvc5 Authors: cvc5 developer documentation. https:\/\/github.com\/cvc5\/cvc5\/wiki (2021)"},{"key":"24_CR7","unstructured":"cvc5 Authors: cvc5 SMT-COMP 2021 Single Query run script. https:\/\/github.com\/cvc5\/cvc5\/blob\/smtcomp2021\/contrib\/competitions\/smt-comp\/run-script-smtcomp-current (2021)"},{"key":"24_CR8","unstructured":"cvc5 Authors: cvc5 user documentation. https:\/\/cvc5.github.io (2021)"},{"key":"24_CR9","unstructured":"Authors, C.: CVC4 SMT-COMP 2020 Single Query run script. https:\/\/github.com\/CVC4\/CVC4\/blob\/smtcomp2020\/contrib\/competitions\/smt-comp\/run-script-smtcomp-current (2020)"},{"key":"24_CR10","doi-asserted-by":"publisher","unstructured":"Backes, J., Berrueco, U., Bray, T., Brim, D., Cook, B., Gacek, A., Jhala, R., Luckow, K.S., McLaughlin, S., Menon, M., Peebles, D., Pugalia, U., Rungta, N., Schlesinger, C., Schodde, A., Tanuku, A., Varming, C., Viswanathan, D.: Stratified abstraction of access control policies. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12224, pp. 165\u2013176. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_9","DOI":"10.1007\/978-3-030-53288-8_9"},{"key":"24_CR11","doi-asserted-by":"publisher","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K.S., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using SMT. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp.\u00a01\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"24_CR12","unstructured":"Bansal, K.: A branching heuristic in cvc4 smt solver. https:\/\/kshitij.io\/articles\/cvc4-branching-heuristic.pdf (2012)"},{"key":"24_CR13","unstructured":"Bansal, K., Barrett, C.W., Reynolds, A., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. CoRR abs\/1702.06259 (2017), http:\/\/arxiv.org\/abs\/1702.06259"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M.M.Y., Niemetz, A., Noetzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: Artifact for Paper cvc5: A Versatile and Industrial-Strength SMT Solver (Nov 2021). https:\/\/doi.org\/10.5281\/zenodo.5740365, https:\/\/doi.org\/10.5281\/zenodo.5740365","DOI":"10.5281\/zenodo.5740365"},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning 64(3), 485\u2013510 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09502-y","DOI":"10.1007\/s10817-018-09502-y"},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10206, pp. 214\u2013230 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_13","DOI":"10.1007\/978-3-662-54580-5_13"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Reynolds, A., Larraz, D., Tinelli, C.: Extending enumerative function synthesis via smt-driven classification. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. pp. 212\u2013220. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894267","DOI":"10.23919\/FMCAD.2019.8894267"},{"key":"24_CR18","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 11716, pp. 35\u201354. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_3","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"24_CR19","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de\u00a0Boer, F.S., Bonsangue, M.M., Graf, S., de\u00a0Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures. Lecture Notes in Computer Science, vol.\u00a04111, pp. 364\u2013387. Springer (2005). https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: International Symposium on Formal Methods for Components and Objects. pp. 364\u2013387. Springer (2005)","DOI":"10.1007\/11804192_17"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV. Lecture Notes in Computer Science, vol.\u00a06806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2020), http:\/\/smt-lib.org","DOI":"10.3233\/FAIA201017"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR \u201906). Lecture Notes in Computer Science, vol.\u00a04246, pp. 512\u2013526. Springer-Verlag (Nov 2006), phnom Penh, Cambodia","DOI":"10.1007\/11916277_35"},{"key":"24_CR24","doi-asserted-by":"publisher","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. JSAT 3(1-2), 21\u201346 (2007). https:\/\/doi.org\/10.3233\/sat190028","DOI":"10.3233\/sat190028"},{"key":"24_CR25","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a03114, pp. 515\u2013518. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_49","DOI":"10.1007\/978-3-540-27813-9_49"},{"key":"24_CR27","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a04590, pp. 298\u2013302. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_34","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"24_CR28","unstructured":"Beazley, D.M.: SWIG: an easy to use tool for integrating scripting languages with C and C++. In: Diekhans, M., Roseman, M. (eds.) Fourth Annual USENIX Tcl\/Tk Workshop 1996, Monterey, California, USA, July 10-13, 1996. USENIX Association (1996), https:\/\/www.usenix.org\/legacy\/publications\/library\/proceedings\/tcl96\/beazley.html"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Behnel, S., Bradshaw, R., Citro, C., Dalcin, L., Seljebotn, D.S., Smith, K.: Cython: The best of both worlds. Computing in Science & Engineering 13(2), 31\u201339 (2011)","DOI":"10.1109\/MCSE.2010.118"},{"key":"24_CR30","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"24_CR31","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06803, pp. 116\u2013130. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"24_CR33","doi-asserted-by":"publisher","unstructured":"Bouchet, M., Cook, B., Cutler, B., Druzkina, A., Gacek, A., Hadarean, L., Jhala, R., Marshall, B., Peebles, D., Rungta, N., Schlesinger, C., Stephens, C., Varming, C., Warfield, A.: Block public access: trust safety verification of access control policies. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020. pp. 281\u2013291. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409728","DOI":"10.1145\/3368089.3409728"},{"key":"24_CR34","doi-asserted-by":"publisher","unstructured":"Bouton, T., de\u00a0Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: An Open, Trustable and Efficient SMT-Solver. In: Schmidt, R.A. (ed.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol.\u00a05663, pp. 151\u2013156. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"24_CR35","doi-asserted-by":"publisher","unstructured":"Bouton, T., Oliveira, D.C.B.D., D\u00e9harbe, D., Fontaine, P.: veriT: An open, trustable and efficient smt-solver. In: Schmidt, R.A. (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05663, pp. 151\u2013156. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"24_CR36","doi-asserted-by":"publisher","unstructured":"Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C.W., Tinelli, C.: Invertibility conditions for floating-point formulas. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11562, pp. 116\u2013136. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_8","DOI":"10.1007\/978-3-030-25543-5_8"},{"key":"24_CR37","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: TACAS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I. LNCS, vol. 11427, pp. 79\u201398. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_5","DOI":"10.1007\/978-3-030-17462-0_5"},{"key":"24_CR38","doi-asserted-by":"publisher","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA. pp. 69\u201376. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351141","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Bromberger, M., Weidenbach, C.: Fast cube tests for LIA constraint solving. In: IJCAR. Lecture Notes in Computer Science, vol.\u00a09706, pp. 116\u2013132. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_9"},{"key":"24_CR40","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. pp. 209\u2013224. USENIX Association (2008), http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"24_CR41","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"24_CR42","doi-asserted-by":"publisher","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 510\u2013517. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"24_CR43","doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J.: Weakly equivalent arrays. In: FroCos. Lecture Notes in Computer Science, vol.\u00a09322, pp. 119\u2013134. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_8"},{"key":"24_CR44","doi-asserted-by":"publisher","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: Smtinterpol: An interpolating SMT solver. In: Donaldson, A.F., Parker, D. (eds.) Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07385, pp. 248\u2013254. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"24_CR45","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 58\u201375 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_4","DOI":"10.1007\/978-3-662-54577-5_4"},{"key":"24_CR46","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Proc.\u00a0TACAS. Lecture Notes in Computer Science, vol.\u00a07795, pp. 93\u2013107. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"24_CR47","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. (JAIR) 40, 701\u2013728 (2011). https:\/\/doi.org\/10.1613\/jair.3196","DOI":"10.1613\/jair.3196"},{"key":"24_CR48","doi-asserted-by":"publisher","unstructured":"Cook, B.: Formal reasoning about the security of amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 38\u201347. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"24_CR49","unstructured":"Corbett, R.: Gnu bison (2021), https:\/\/www.gnu.org\/software\/bison\/"},{"key":"24_CR50","doi-asserted-by":"publisher","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S.A. (eds.) Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09340, pp. 360\u2013368. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"24_CR51","doi-asserted-by":"publisher","unstructured":"Craig, W.: Linear reasoning. A new form of the herbrand-gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957). https:\/\/doi.org\/10.2307\/2963593","DOI":"10.2307\/2963593"},{"key":"24_CR52","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c - A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07504, pp. 233\u2013247. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"24_CR53","doi-asserted-by":"crossref","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","DOI":"10.1145\/1066100.1066102"},{"key":"24_CR54","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. Formal Methods Syst. Des. 39(3), 246\u2013260 (2011)","DOI":"10.1007\/s10703-011-0127-z"},{"key":"24_CR55","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a08559, pp. 737\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"24_CR56","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de\u00a0Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: CAV. Lecture Notes in Computer Science, vol.\u00a04144, pp. 81\u201394. Springer (2006)","DOI":"10.1007\/11817963_11"},{"key":"24_CR57","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: SAT. Lecture Notes in Computer Science, vol.\u00a02919, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"24_CR58","doi-asserted-by":"publisher","unstructured":"Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: Smtcoq: A plug-in for integrating SMT solvers into coq. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 10427, pp. 126\u2013133. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"24_CR59","doi-asserted-by":"publisher","unstructured":"England, M., Bradford, R.J., Davenport, J.H., Wilson, D.J.: Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Hong, H., Yap, C. (eds.) Mathematical Software - ICMS 2014 - 4th International Congress, Seoul, South Korea, August 5-9, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08592, pp. 450\u2013457. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-662-44199-2_68","DOI":"10.1007\/978-3-662-44199-2_68"},{"key":"24_CR60","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J., Paskevich, A.: Why3 - where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07792, pp. 125\u2013128. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"24_CR61","doi-asserted-by":"publisher","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04590, pp. 519\u2013531. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"24_CR62","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: SAGE: whitebox fuzzing for security testing. Commun. ACM 55(3), 40\u201344 (2012). https:\/\/doi.org\/10.1145\/2093548.2093564","DOI":"10.1145\/2093548.2093564"},{"key":"24_CR63","unstructured":"Griggio, A.: An Effective SMT Engine for Formal Verification. Ph.D. thesis, University of Trento, Italy (2009)"},{"key":"24_CR64","doi-asserted-by":"crossref","unstructured":"Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. Journal on Satisfiability, Boolean Modeling and Computation 8(1-2), 1\u201327 (2012)","DOI":"10.3233\/SAT190086"},{"key":"24_CR65","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. pp. 62\u201373. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993506","DOI":"10.1145\/1993498.1993506"},{"key":"24_CR66","unstructured":"Hadarean, L.: An efficient and trustworthy theory solver for bit-vectors in satisfiability modulo theories. Ph.D. thesis, Citeseer (2015)"},{"key":"24_CR67","doi-asserted-by":"publisher","unstructured":"Hadarean, L., Barrett, C.W., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the theory of fixed-width bit-vectors. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09450, pp. 340\u2013355. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_24","DOI":"10.1007\/978-3-662-48899-7_24"},{"key":"24_CR68","doi-asserted-by":"publisher","unstructured":"Hajdu, \u00c1., Jovanovic, D.: solc-verify: A modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers. Lecture Notes in Computer Science, vol. 12031, pp. 161\u2013179. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"24_CR69","doi-asserted-by":"crossref","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association for Computing Machinery 40(1), 143\u2013184 (Jan 1993)","DOI":"10.1145\/138027.138060"},{"key":"24_CR70","doi-asserted-by":"publisher","unstructured":"Hauzar, D., March\u00e9, C., Moy, Y.: Counterexamples from proof failures in SPARK. In: Nicola, R.D., eva K\u00fchn (eds.) Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09763, pp. 215\u2013233. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_15","DOI":"10.1007\/978-3-319-41591-8_15"},{"key":"24_CR71","doi-asserted-by":"crossref","unstructured":"Hughes, R.J.M.: Super combinators: a new implementation method for applicative languages. In: Symposium on LISP and Functional Programming. pp. 1\u201310 (1982)","DOI":"10.1145\/800068.802129"},{"key":"24_CR72","doi-asserted-by":"publisher","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: An SMT solver for multi-core and cloud computing. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09710, pp. 547\u2013553. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_35","DOI":"10.1007\/978-3-319-40970-2_35"},{"key":"24_CR73","unstructured":"Iosif, R., Serban, C., Reynolds, A., Sighireanu, M.: Encoding separation logic in smt-lib v2.5 (2018)"},{"key":"24_CR74","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., Barrett, C.W.: Polite theories revisited. In: LPAR (Yogyakarta). Lecture Notes in Computer Science, vol.\u00a06397, pp. 402\u2013416. Springer (2010)","DOI":"10.1007\/978-3-642-16242-8_29"},{"key":"24_CR75","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., Barrett, C.W.: Being careful about theory combination. Formal Methods Syst. Des. 42(1), 67\u201390 (2013)","DOI":"10.1007\/s10703-012-0159-z"},{"key":"24_CR76","unstructured":"Jovanovic, D., Dutertre, B.: Libpoly: A library for reasoning about polynomials. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22 - 23, 2017. CEUR Workshop Proceedings, vol.\u00a01889, pp. 28\u201339. CEUR-WS.org (2017), http:\/\/ceur-ws.org\/Vol-1889\/paper3.pdf"},{"key":"24_CR77","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for dpll(t)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016. pp. 93\u2013100. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886666","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"24_CR78","unstructured":"King, T.: Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic. Ph.D. thesis, New York University (2014)"},{"key":"24_CR79","doi-asserted-by":"crossref","unstructured":"King, T., Barrett, C.W., Dutertre, B.: Simplex with sum of infeasibilities for SMT. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp. 189\u2013196. IEEE (2013), https:\/\/ieeexplore.ieee.org\/document\/6679409\/","DOI":"10.1109\/FMCAD.2013.6679409"},{"key":"24_CR80","doi-asserted-by":"publisher","unstructured":"King, T., Barrett, C.W., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. pp. 139\u2013146. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987606","DOI":"10.1109\/FMCAD.2014.6987606"},{"key":"24_CR81","doi-asserted-by":"publisher","unstructured":"Leino, K.M.: Accessible software verification with dafny. IEEE Software 34(06), 94\u201397 (nov 2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","DOI":"10.1109\/MS.2017.4121212"},{"key":"24_CR82","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a06355, pp. 348\u2013370. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"24_CR83","unstructured":"Liang, S.: The Java Native interface : programmer\u2019s guide and specification \/ Sheng Liang. Java series, Addison-Wesley, Reading, Mass. ; Harlow, England (1999)"},{"key":"24_CR84","doi-asserted-by":"crossref","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C.W., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 646\u2013662. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"24_CR85","doi-asserted-by":"crossref","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.W.: A decision procedure for regular membership and length constraints over unbounded strings. In: FroCos. Lecture Notes in Computer Science, vol.\u00a09322, pp. 135\u2013150. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"24_CR86","doi-asserted-by":"publisher","unstructured":"Mattarei, C., Mann, M., Barrett, C.W., Daly, R.G., Huff, D., Hanrahan, P.: Cosa: Integrated verification for agile hardware design. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. pp.\u00a01\u20135. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603014","DOI":"10.23919\/FMCAD.2018.8603014"},{"key":"24_CR87","doi-asserted-by":"publisher","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.W.: Relational constraint solving in SMT. In: de\u00a0Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 148\u2013165. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_10","DOI":"10.1007\/978-3-319-63046-5_10"},{"key":"24_CR88","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12699, pp. 625\u2013635. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"24_CR89","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04603, pp. 183\u2013198. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"24_CR90","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24, https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"24_CR91","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD. pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"24_CR92","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs\/2006.01621 (2020), https:\/\/arxiv.org\/abs\/2006.01621"},{"key":"24_CR93","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Ternary propagation-based local search for more bit-precise reasoning. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. pp. 214\u2013224. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_29","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_29"},{"key":"24_CR94","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3), 608\u2013636 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0295-6","DOI":"10.1007\/s10703-017-0295-6"},{"key":"24_CR95","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C.W., Tinelli, C.: On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57(1), 87\u2013115 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00359-9","DOI":"10.1007\/s10703-020-00359-9"},{"key":"24_CR96","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C.W., Tinelli, C.: Syntax-guided quantifier instantiation. In: Groote, J.F., Larsen, K.G. (eds.) 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, vol. 12652, pp. 145\u2013163. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_8","DOI":"10.1007\/978-3-030-72013-1_8"},{"key":"24_CR97","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C.W., Tinelli, C.: Towards bit-width-independent proofs in SMT solvers. In: Fontaine, P. (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11716, pp. 366\u2013384. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_22","DOI":"10.1007\/978-3-030-29436-6_22"},{"key":"24_CR98","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2 , btormc and boolector 3.0. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 587\u2013595. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"24_CR99","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract davis\u2013putnam\u2013logemann\u2013loveland procedure to dpll(T). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","DOI":"10.1145\/1217856.1217859"},{"key":"24_CR100","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol.\u00a02283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"24_CR101","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C.W., Tinelli, C.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11628, pp. 279\u2013297. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_20","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"24_CR102","unstructured":"Organizers, S.C.: SMT-COMP 2021. https:\/\/smt-comp.github.io\/2021\/ (2021)"},{"key":"24_CR103","unstructured":"Organizers, S.C.: SyGuS-Comp 2019. https:\/\/sygus.org\/comp\/2019\/ (2021)"},{"key":"24_CR104","unstructured":"Padhi, S., Polgreen, E., Raghothaman, M., Reynolds, A., Udupa, A.: The sygus language standard version 2.1 (2021)"},{"key":"24_CR105","unstructured":"Parr, T.: ANTLRv3 (2021), https:\/\/www.antlr3.org\/"},{"key":"24_CR106","unstructured":"Paxson, V.: Flex lexical analyser generator (2021), https:\/\/github.com\/westes\/flex"},{"key":"24_CR107","doi-asserted-by":"publisher","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 2008, Proceedings. Lecture Notes in Computer Science, vol.\u00a04905, pp. 218\u2013232. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78163-9_20","DOI":"10.1007\/978-3-540-78163-9_20"},{"key":"24_CR108","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: FroCoS. Lecture Notes in Computer Science, vol.\u00a03717, pp. 48\u201364. Springer (2005)","DOI":"10.1007\/11559306_3"},{"key":"24_CR109","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10806, pp. 112\u2013131. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"24_CR110","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., Larraz, D., Tinelli, C.: Scalable algorithms for abduction via enumerative syntax-guided synthesis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12166, pp. 141\u2013160. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_9","DOI":"10.1007\/978-3-030-51074-9_9"},{"key":"24_CR111","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C.W., Tinelli, C.: cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11562, pp. 74\u201383. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"24_CR112","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09195, pp. 197\u2013213. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_13","DOI":"10.1007\/978-3-319-21401-6_13"},{"key":"24_CR113","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09706, pp. 133\u2013151. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_10","DOI":"10.1007\/978-3-319-40229-1_10"},{"key":"24_CR114","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09207, pp. 198\u2013216. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"24_CR115","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Artho, C., Legay, A., Peled, D. (eds.) Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09938, pp. 244\u2013261 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_16","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"24_CR116","doi-asserted-by":"publisher","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3), 500\u2013532 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0290-y","DOI":"10.1007\/s10703-017-0290-y"},{"key":"24_CR117","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a08931, pp. 80\u201398. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"24_CR118","doi-asserted-by":"crossref","unstructured":"Reynolds, A., N\u00f6tzli, A., Barrett, C.W., Tinelli, C.: High-level abstractions for simplifying extended string constraints in SMT. In: CAV (2). Lecture Notes in Computer Science, vol. 11562, pp. 23\u201342. Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_2"},{"key":"24_CR119","doi-asserted-by":"crossref","unstructured":"Reynolds, A., N\u00f6tzli, A., Barrett, C.W., Tinelli, C.: A decision procedure for string to code point conversion. In: IJCAR (1). Lecture Notes in Computer Science, vol. 12166, pp. 218\u2013237. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_13"},{"key":"24_CR120","unstructured":"Reynolds, A., N\u00f6tzli, A., Barrett, C.W., Tinelli, C.: Reductions for strings and regular expressions revisited. In: FMCAD. pp. 225\u2013235. IEEE (2020)"},{"key":"24_CR121","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krstic, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08044, pp. 640\u2013655. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_42","DOI":"10.1007\/978-3-642-39799-8_42"},{"key":"24_CR122","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krstic, S., Deters, M., Barrett, C.W.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07898, pp. 377\u2013391. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_26","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"24_CR123","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C.W.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Bras\u00edlia, Brazil, September 27-29, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10483, pp. 22\u201340. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_2","DOI":"10.1007\/978-3-319-66167-4_2"},{"key":"24_CR124","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., de\u00a0Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. pp. 195\u2013202. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987613","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"24_CR125","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.W.: Datatypes with shared selectors. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10900, pp. 591\u2013608. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_39","DOI":"10.1007\/978-3-319-94205-6_39"},{"key":"24_CR126","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Woo, M., Barrett, C.W., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: CAV (2). Lecture Notes in Computer Science, vol. 10427, pp. 453\u2013474. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_24"},{"key":"24_CR127","doi-asserted-by":"publisher","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic program optimization. Commun. ACM 59(2), 114\u2013122 (2016). https:\/\/doi.org\/10.1145\/2863701","DOI":"10.1145\/2863701"},{"key":"24_CR128","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: Towards a generic SMT proof format (extended abstract). In: Keller, C., Fleury, M. (eds.) Workshop on Proof eXchange for Theorem Proving (PxTP). EPTCS, vol.\u00a0336, pp. 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6, https:\/\/doi.org\/10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"key":"24_CR129","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 12699, pp. 450\u2013467. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26","DOI":"10.1007\/978-3-030-79876-5_26"},{"key":"24_CR130","doi-asserted-by":"publisher","unstructured":"Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12166, pp. 238\u2013255. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_14","DOI":"10.1007\/978-3-030-51074-9_14"},{"key":"24_CR131","unstructured":"Soos, M.: CryptoMiniSat. https:\/\/github.com\/msoos\/cryptominisat (2020)"},{"key":"24_CR132","doi-asserted-by":"publisher","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol.\u00a02404, pp. 500\u2013504. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_40","DOI":"10.1007\/3-540-45657-0_40"},{"key":"24_CR133","doi-asserted-by":"publisher","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods in System Design 42(1), 91\u2013118 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0163-3","DOI":"10.1007\/s10703-012-0163-3"},{"key":"24_CR134","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"24_CR135","doi-asserted-by":"publisher","unstructured":"Tillmann, N., de\u00a0Halleux, J.: Pex-white box test generation for .net. In: Beckert, B., H\u00e4hnle, R. (eds.) Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a04966, pp. 134\u2013153. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_10","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"24_CR136","unstructured":"Trentin, P.: Optimization Modulo Theories with OptiMathSAT. Ph.D. thesis, University of Trento (2019)"},{"key":"24_CR137","doi-asserted-by":"publisher","unstructured":"Zhong, J.E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C.W., Dill, D.L.: The move prover. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12224, pp. 137\u2013150. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_7","DOI":"10.1007\/978-3-030-53288-8_7"},{"key":"24_CR138","doi-asserted-by":"crossref","unstructured":"Zohar, Y., Irfan, A., Mann, M., Niemetz, A., N\u00f6tzli, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Bit-Precise Reasoning via Int-Blasting, to appear in the proceedings of VMCAI 2022","DOI":"10.1007\/978-3-030-94583-1_24"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:25:32Z","timestamp":1648535132000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":138,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}