{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:30Z","timestamp":1784797590626,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    A DFA separates two disjoint languages\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L_1$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msub>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mn>1<\/mml:mn>\n                          <\/mml:msub>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    and\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L_2$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msub>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mn>2<\/mml:mn>\n                          <\/mml:msub>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    if it accepts every word in\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L_1$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msub>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mn>1<\/mml:mn>\n                          <\/mml:msub>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    and rejects every word in\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L_2$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msub>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mn>2<\/mml:mn>\n                          <\/mml:msub>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . Algorithms for active learning of small separating DFAs have many applications, e.g. for learning network invariants, learning contextual assumptions in compositional verification, learning state machines from large amounts of log data, and learning bug pattern descriptions. We propose a simple active learning algorithm, inspired by\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L^{\\#}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mo>#<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , that learns a minimal separating DFA for disjoint languages\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L_1$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msub>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mn>1<\/mml:mn>\n                          <\/mml:msub>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    and\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$L_2$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msub>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mn>2<\/mml:mn>\n                          <\/mml:msub>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    if one exists. Experiments show that our algorithm significantly outperforms existing active learning algorithms on both randomly generated and industrial benchmarks.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_13","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:14Z","timestamp":1784796434000},"page":"261-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An $$L^{\\#}$$ Based Algorithm for\u00a0Active Learning of\u00a0Minimal Separating Automata"],"prefix":"10.1007","author":[{"given":"Jasper","family":"Laumen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonne","family":"Snel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987). https:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","journal-title":"Inf. Comput."},{"issue":"1\u20132","key":"13_CR2","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/S10994-013-5416-X","volume":"96","author":"B Balle","year":"2014","unstructured":"Balle, B., Carreras, X., Luque, F.M., Quattoni, A.: Spectral learning of weighted automata - a forward-backward perspective. Mach. Learn. 96(1\u20132), 33\u201363 (2014). https:\/\/doi.org\/10.1007\/S10994-013-5416-X","journal-title":"Mach. Learn."},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Bar-Sinai, M., Elyasaf, A., Weiss, G., Weiss, Y.: Provengo: a tool suite for scenario driven model-based testing. In: ASE, pp. 2062\u20132065. IEEE (2023). https:\/\/doi.org\/10.48550\/ARXIV.2308.15938","DOI":"10.48550\/ARXIV.2308.15938"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Computers 21(6), 592\u2013597 (1972). https:\/\/doi.org\/10.1109\/TC.1972.5009015","DOI":"10.1109\/TC.1972.5009015"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Bruy\u00e8re, V., Garhewal, B., P\u00e9rez, G.A., Staquet, G., Vaandrager, F.W.: Active learning of mealy machines with timers. In: Prabhakar, P., Vandin, A. (eds.) QEST+FORMATS 2025. LNCS, vol. 16143. Springer, Cham (2026). https:\/\/doi.org\/10.1007\/978-3-032-05792-1_3","DOI":"10.1007\/978-3-032-05792-1_3"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-00768-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-F Chen","year":"2009","unstructured":"Chen, Y.-F., Farzan, A., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Learning minimal separating DFA\u2019s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 31\u201345. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_3"},{"issue":"3","key":"13_CR7","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"T Chow","year":"1978","unstructured":"Chow, T.: Testing software design modeled by finite-state machines. IEEE Trans. Software Eng. 4(3), 178\u2013187 (1978). https:\/\/doi.org\/10.1109\/TSE.1978.231496","journal-title":"IEEE Trans. Software Eng."},{"issue":"5","key":"13_CR8","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3419404","volume":"64","author":"L D\u2019Antoni","year":"2021","unstructured":"D\u2019Antoni, L., Veanes, M.: Automata modulo theories. Commun. ACM 64(5), 86\u201395 (2021). https:\/\/doi.org\/10.1145\/3419404","journal-title":"Commun. ACM"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Dierl, S., Fiterau-Brostean, P., Howar, F., Jonsson, B., Sagonas, K., T\u00e5quist, F.: Scalable tree-based register automata learning. In: Finkbeiner, B., Kov\u00e1cs, L. (eds) TACAS 2024. LNCS, vol 14571. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_5","DOI":"10.1007\/978-3-031-57249-4_5"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Geuvers, H., Jacobs, B.: Relating apartness and bisimulation. Logical Methods in Computer Science 17(3) (2021). https:\/\/doi.org\/10.46298\/lmcs-17(3:15)2021","DOI":"10.46298\/lmcs-17(3:15)2021"},{"issue":"3","key":"13_CR11","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1016\/S0019-9958(78)90562-4","volume":"37","author":"EM Gold","year":"1978","unstructured":"Gold, E.M.: Complexity of automaton identification from given data. Inf. Control 37(3), 302\u2013320 (1978). https:\/\/doi.org\/10.1016\/S0019-9958(78)90562-4","journal-title":"Inf. Control"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/11814771_40","volume-title":"Automated Reasoning","author":"O Grinchtein","year":"2006","unstructured":"Grinchtein, O., Leucker, M., Piterman, N.: Inferring NETWORK INVARIANTS AUTOMATICALLY. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 483\u2013497. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_40"},{"key":"13_CR13","series-title":"10.1007\/978-3-642-15488-1_7","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-15488-1_7","volume-title":"Grammatical Inference: Theoretical Results and Applications","author":"MJH Heule","year":"2010","unstructured":"Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., Garc\u00eda, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 66\u201379. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15488-1_7"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press (2010). https:\/\/doi.org\/10.1017\/CBO9781139194655","DOI":"10.1017\/CBO9781139194655"},{"issue":"2","key":"13_CR15","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0166-218X(96)00025-X","volume":"74","author":"Y Ishigami","year":"1997","unstructured":"Ishigami, Y., Tani, S.: VC-dimensions of finite automata and commutative finite automata with k letters and n states. Discret. Appl. Math. 74(2), 123\u2013134 (1997). https:\/\/doi.org\/10.1016\/S0166-218X(96)00025-X","journal-title":"Discret. Appl. Math."},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-17502-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Jasper","year":"2019","unstructured":"Jasper, M., et al.: RERS 2019: combining synthesis with real-world models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 101\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_7"},{"key":"13_CR17","unstructured":"Laumen, J., Snel, L., Vaandrager, F.: An $$L^\\#$$ based algorithm for active learning of minimal separating automata (May 2026). https:\/\/arxiv.org\/abs\/2605.15294"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Lee, M., So, S., Oh, H.: Synthesizing regular expressions from examples for introductory automata assignments. In: Fischer, B., Schaefer, I. (eds.) Proceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2016, Amsterdam, The Netherlands, 31 October - 1 November 2016, pp. 70\u201380. ACM (2016). https:\/\/doi.org\/10.1145\/2993236.2993244","DOI":"10.1145\/2993236.2993244"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-642-34026-0_39","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"M Leucker","year":"2012","unstructured":"Leucker, M., Neider, D.: Learning minimal deterministic automata from inexperienced teachers. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 524\u2013538. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_39"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Moeller, M., Wiener, T., Solko-Breslin, A., Koch, C., Foster, N., Silva, A.: Automata learning with an incomplete teacher. In: ECOOP. LIPIcs, vol.\u00a0263, pp. 21:1\u201321:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2023.21","DOI":"10.4230\/LIPICS.ECOOP.2023.21"},{"key":"13_CR21","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"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Mu\u0161kardin, E., Aichernig, B., Pferscher, A., Tappler, M.: Aalpy: an active automata learning library. Innovat. Syst. Softw. Eng. 18, 1\u201310 (2022). https:\/\/doi.org\/10.1007\/s11334-022-00449-3","DOI":"10.1007\/s11334-022-00449-3"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-33386-6_28","volume-title":"Automated Technology for Verification and Analysis","author":"D Neider","year":"2012","unstructured":"Neider, D.: Computing minimal separating dfas and regular invariants using SAT and SMT solvers. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 354\u2013369. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_28"},{"issue":"1\/2","key":"13_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1023\/A:1010828029885","volume":"44","author":"AL Oliveira","year":"2001","unstructured":"Oliveira, A.L., Silva, J.P.M.: Efficient algorithms for the inference of minimum size DFAs. Mach. Learn. 44(1\/2), 93\u2013119 (2001). https:\/\/doi.org\/10.1023\/A:1010828029885","journal-title":"Mach. Learn."},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Oncina, J., Garc\u00eda, P.: Inferring regular languages in polynomial update time. World Sci.(1992). https:\/\/doi.org\/10.1142\/9789812797902_0004","DOI":"10.1142\/9789812797902_0004"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Pena, J.M., Oliveira, A.L.: A new algorithm for exact reduction of incompletely specified finite state machines. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18(11), 1619\u20131632 (1999). https:\/\/doi.org\/10.1109\/43.806807","DOI":"10.1109\/43.806807"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Pfleeger, C.P.: State reduction in incompletely specified finite-state machines. IEEE Trans. Computers 22(12), 1099\u20131102 (1973). https:\/\/doi.org\/10.1109\/T-C.1973.223655","DOI":"10.1109\/T-C.1973.223655"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Rot, J., Wi\u00dfmann, T.: Bisimilar states in uncertain structures. In: 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023), pp. 12:1\u201312:17. Leibniz International Proceedings in Informatics (Sep 2023). https:\/\/doi.org\/10.4230\/LIPIcs.CALCO.2023.12","DOI":"10.4230\/LIPIcs.CALCO.2023.12"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-319-77313-1_14","volume-title":"Language and Automata Theory and Applications","author":"R Smetsers","year":"2018","unstructured":"Smetsers, R., Fiter\u0103u-Bro\u015ftean, P., Vaandrager, F.: Model learning as a satisfiability modulo theories problem. In: Klein, S.T., Mart\u00edn-Vide, C., Shapira, D. (eds.) LATA 2018. LNCS, vol. 10792, pp. 182\u2013194. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77313-1_14"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, 2 edn. Cambridge University Press (2000). https:\/\/doi.org\/10.1017\/CBO9781139168717","DOI":"10.1017\/CBO9781139168717"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-99524-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Vaandrager","year":"2022","unstructured":"Vaandrager, F., Garhewal, B., Rot, J., Wi\u00dfmann, T.: A new approach for active automata learning based on apartness. In: TACAS 2022. LNCS, vol. 13243, pp. 223\u2013243. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_12"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Vaandrager, F.W., Sanders, M.: L$$ ^{\\#}$$ for DFAs. In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M. (eds.) Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III. LNCS, vol. 15262, pp. 155\u2013172. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_8","DOI":"10.1007\/978-3-031-75778-5_8"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Vasilevskii, M.: Failure diagnosis of automata. Cybernetics and System Analysis 9(4), 653\u2013665 (1973). https:\/\/doi.org\/10.1007\/BF01068590, (Translated from Kibernetika, No. 4, pp. 98-108, July-August, 1973)","DOI":"10.1007\/BF01068590"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Verwer, S., Hammerschmidt, C.A.: flexfringe: a passive automaton learning package. In: 2017 IEEE International Conference on Software Maintenance and Evolution, ICSME 2017, Shanghai, China, 17-22 September 2017. pp. 638\u2013642. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ICSME.2017.58","DOI":"10.1109\/ICSME.2017.58"},{"key":"13_CR35","unstructured":"Walinga, H., Baumgartner, R., Verwer, S.: Database-assisted automata learning. CoRR arXiv: abs\/2406.07208 (2024)"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Yaacov, T., Weiss, G., Amram, G., Hayoun, A.: Automata models for effective bug pattern description. In: 28th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2025, Grand Rapids, MI, USA, 5-10 October 2025. pp. 119\u2013129. IEEE (2025). https:\/\/doi.org\/10.1109\/MODELS67397.2025.00017","DOI":"10.1109\/MODELS67397.2025.00017"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:17Z","timestamp":1784796437000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}