{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:29Z","timestamp":1771024229450,"version":"3.50.1"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031402463","type":"print"},{"value":"9783031402470","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-40247-0_15","type":"book-chapter","created":{"date-parts":[[2023,8,9]],"date-time":"2023-08-09T08:02:54Z","timestamp":1691568174000},"page":"206-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verified Verifying: SMT-LIB for\u00a0Strings in\u00a0Isabelle"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6759-3304","authenticated-orcid":false,"given":"Kevin","family":"Lotz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4650-1110","authenticated-orcid":false,"given":"Mitja","family":"Kulczynski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Nowotka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9623-0748","authenticated-orcid":false,"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9212-6150","authenticated-orcid":false,"given":"Anders","family":"Schlichtkrull","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,8,10]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: TRAU: SMT solver for string constraints. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20135. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Backes, J., et al.: Semantic-based automated reasoning for AWS access policies using SMT. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20139 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022, Part I. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-031-10769-6_3","volume-title":"IJCAR 2022","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 15\u201335. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3"},{"key":"15_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). http:\/\/www.SMT-LIB.org"},{"key":"15_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Satisfiability Modulo Theories","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability Modulo Theories. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 55\u201359. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-030-81688-9_14","volume-title":"Computer Aided Verification","author":"M Berzish","year":"2021","unstructured":"Berzish, M., et al.: An SMT solver for regular expressions and linear arithmetic over string length. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 289\u2013312. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307\u2013321. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_27"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Fleury, M., Lammich, P., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. J. Autom. Reason. 61(1-4), 333\u2013365 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9455-7","DOI":"10.1007\/s10817-018-9455-7"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-40229-1_4","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 25\u201344. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_4"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Fleury, M., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, 19\u201325 August 2017, pp. 4786\u20134790. ijcai.org (2017). https:\/\/doi.org\/10.24963\/ijcai.2017\/667","DOI":"10.24963\/ijcai.2017\/667"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14"},{"issue":"4","key":"15_CR14","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM (JACM) 11(4), 481\u2013494 (1964)","journal-title":"J. ACM (JACM)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Chen, T., Hague, M., Lin, A.W., R\u00fcmmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. In: Proceedings of the ACM on Programming Languages 3(POPL), pp. 1\u201330 (2019)","DOI":"10.1145\/3290362"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-30806-3_8","volume-title":"Reachability Problems","author":"JD Day","year":"2019","unstructured":"Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 93\u2013106. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"15_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2685616","volume":"24","author":"H Eldib","year":"2014","unstructured":"Eldib, H., Wang, C., Schaumont, P.: Formal verification of software countermeasures against side-channel attacks. ACM Trans. Softw. Eng. Methodol. (TOSEM) 24(2), 1\u201324 (2014)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-030-20652-9_10","volume-title":"NASA Formal Methods","author":"M Fleury","year":"2019","unstructured":"Fleury, M.: Optimizing a verified SAT solver. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 148\u2013165. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_10"},{"key":"15_CR20","unstructured":"Fleury, M.: Formalization of logical calculi in Isabelle\/HOL. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2020). https:\/\/tel.archives-ouvertes.fr\/tel-02963301"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Fleury, M., Blanchette, J.C., Lammich, P.: A verified SAT solver with watched literals using imperative HOL. In: Andronick, J., Felty, A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, 8\u20139 January 2018, pp. 158\u2013171. ACM (2018). https:\/\/doi.org\/10.1145\/3167080","DOI":"10.1145\/3167080"},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Fleury, M., Schurr, H.: Reconstructing veriT proofs in Isabelle\/HOL. In: Reis, G., Barbosa, H. (eds.) Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, 26 August 2019. EPTCS, vol. 301, pp. 36\u201350 (2019). https:\/\/doi.org\/10.4204\/EPTCS.301.6","DOI":"10.4204\/EPTCS.301.6"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Fleury, M., Weidenbach, C.: A verified SAT solver framework including optimization and partial valuations. In: Albert, E., Kov\u00e1cs, L. (eds.) LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, 22\u201327 May 2020. EPiC Series in Computing, vol. 73, pp. 212\u2013229. EasyChair (2020). https:\/\/doi.org\/10.29007\/96wb","DOI":"10.29007\/96wb"},{"issue":"6","key":"15_CR24","doi-asserted-by":"publisher","first-page":"81","DOI":"10.3390\/electronics7060081","volume":"7","author":"T Grimm","year":"2018","unstructured":"Grimm, T., Lettnin, D., H\u00fcbner, M.: A survey on formal verification techniques for safety-critical systems-on-chip. Electronics 7(6), 81 (2018)","journal-title":"Electronics"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-34175-6_2","volume-title":"Programming Languages and Systems","author":"H Hojjat","year":"2019","unstructured":"Hojjat, H., R\u00fcmmer, P., Shamakhi, A.: On strings in software model checking. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 19\u201330. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_2"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Holub, V., Starosta, V.: Formalization of basic combinatorics on words. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 22:1\u201322:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.22. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13917","DOI":"10.4230\/LIPIcs.ITP.2021.22"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Kan, S., Lin, A.W., R\u00fcmmer, P., Schrader, M.: CertiStr: a certified string solver. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 210\u2013224 (2022)","DOI":"10.1145\/3497775.3503691"},{"key":"15_CR28","unstructured":"Krauss, A., Nipkow, T.: Regular sets and expressions. Archive of Formal Proofs, May 2010. https:\/\/isa-afp.org\/entries\/Regular-Sets.html, Formal proof development"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. J. Autom. Reason. 49(1), 95\u2013106 (2011). https:\/\/doi.org\/10.1007\/s10817-011-9223-4","DOI":"10.1007\/s10817-011-9223-4"},{"key":"15_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-031-15077-7_8","volume-title":"Model Checking Software","author":"M Kulczynski","year":"2022","unstructured":"Kulczynski, M., Lotz, K., Nowotka, D., Poulsen, D.B.: Solving string theories involving regular membership predicates using SAT. In: Legunsen, O., Rosu, G. (eds.) Model Checking Software. LNCS, vol. 13255, pp. 134\u2013151. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15077-7_8"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: The power of string solving: simplicity of comparison. In: Proceedings of the IEEE\/ACM 1st International Conference on Automation of Software Test, pp. 85\u201388 (2020)","DOI":"10.1145\/3387903.3389317"},{"key":"15_CR32","unstructured":"Lescuyer, S.: Formalizing and implementing a reflexive tactic for automated deduction in Coq. (Formalisation et developpement d\u2019une tactique reflexive pour la demonstration automatique en coq). Ph.D. thesis, University of Paris-Sud, Orsay, France (2011). https:\/\/tel.archives-ouvertes.fr\/tel-00713668"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Maric, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.09.014","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Maric, F., Janicic, P.: Formalization of abstract state transition systems for SAT. Log. Methods Comput. Sci. 7(3) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:19)2011","DOI":"10.2168\/LMCS-7(3:19)2011"},{"key":"15_CR35","unstructured":"Mari\u0107, F.: Formal verification of modern sat solvers. Archive of Formal Proofs, July 2008. https:\/\/isa-afp.org\/entries\/SATSolverVerification.html, Formal proof development"},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-90870-6_21","volume-title":"Formal Methods","author":"F Mora","year":"2021","unstructured":"Mora, F., Berzish, M., Kulczynski, M., Nowotka, D., Ganesh, V.: Z3str4: a multi-armed string solver. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 389\u2013406. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_21"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"15_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-27940-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Oe","year":"2012","unstructured":"Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: a verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 363\u2013378. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_24"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Redelinghuys, G., Visser, W., Geldenhuys, J.: Symbolic execution of programs with strings. In: Proceedings of the South African Institute for Computer Scientists and Information Technologists Conference, SAICSIT 2012, pp. 139\u2013148 (2012)","DOI":"10.1145\/2389836.2389853"},{"key":"15_CR40","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-13185-1_1","volume-title":"Computer Aided Verification","author":"N Rungta","year":"2022","unstructured":"Rungta, N.: A billion SMT queries a day (invited paper). In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. LNCS, vol. 13371, pp. 3\u201318. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_1"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: 2010 IEEE Symposium on Security and Privacy, pp. 513\u2013528. IEEE (2010)","DOI":"10.1109\/SP.2010.38"},{"key":"15_CR42","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.) Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, 11 July 2021. EPTCS, vol. 336, pp. 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver. In: Haeusler, E.H., del Cerro, L.F. (eds.) Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, LSFA 2010, Natal, Brazil, 31 August 2010. Electronic Notes in Theoretical Computer Science, vol. 269, pp. 3\u201317. Elsevier (2010). https:\/\/doi.org\/10.1016\/j.entcs.2011.03.002","DOI":"10.1016\/j.entcs.2011.03.002"},{"key":"15_CR44","unstructured":"Tinelli, C., Barrett, C., Fontaine, P.: SMT: theory of strings. http:\/\/smtlib.cs.uiowa.edu\/theories-UnicodeStrings.shtml. Accessed 03 Mar 2022"},{"key":"15_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7"},{"key":"15_CR46","unstructured":"Wenzel, M., et al.: The Isabelle\/Isar reference manual (2004)"},{"issue":"1","key":"15_CR47","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/s10703-013-0189-1","volume":"44","author":"F Yu","year":"2013","unstructured":"Yu, F., Alkhalaf, M., Bultan, T., Ibarra, O.H.: Automata-based symbolic string analysis for vulnerability detection. Form. Methods Syst. Des. 44(1), 44\u201370 (2013). https:\/\/doi.org\/10.1007\/s10703-013-0189-1","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"15_CR48","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1093\/jigpal\/jzaa062","volume":"30","author":"AM Zbrzezny","year":"2022","unstructured":"Zbrzezny, A.M., Szymoniak, S., Kurkowski, M.: Practical approach in verification of security systems using satisfiability modulo theories. Log. J. IGPL 30(2), 289\u2013300 (2022)","journal-title":"Log. J. IGPL"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-40247-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,9]],"date-time":"2023-08-09T08:09:21Z","timestamp":1691568561000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-40247-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031402463","9783031402470"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-40247-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"10 August 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CIAA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Implementation and Application of Automata","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Famagusta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wia2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ciaa.emu.edu.tr\/en","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":"EquinOCS","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","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":"20","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":"0","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":"67% - 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":"2-3","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)"}}]}}