{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:46Z","timestamp":1784797546387,"version":"3.55.0"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","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                    Verifying stateful software systems remains challenging due to complex control structures and intricate state interactions, often necessitating pre-existing behavioral models. We introduce , an abstract interpreter that automatically derives sound and precise symbolic finite automata models. In tests on real-world applications,  generates sound and precise automata within minutes and, when employed in dynamic model checking, achieves 1.6\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\times $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>\u00d7<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    \u20133.4\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\times $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>\u00d7<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    code coverage compared to the state of the art. These findings demonstrate that  can effectively connect code to model-based verification for stateful software systems.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_4","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:04Z","timestamp":1784796244000},"page":"73-99","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Sound and Precise Symbolic Automata Model for Stateful Software Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-2713-1409","authenticated-orcid":false,"given":"Xinlong","family":"Wu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2700-9646","authenticated-orcid":false,"given":"Ruiyu","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8297-8998","authenticated-orcid":false,"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., D\u2019Antoni, L., Raghothaman, M.: DReX: a declarative language for efficiently evaluating regular string transformations. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201915, pp. 125\u2013137. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676981","DOI":"10.1145\/2676726.2676981"},{"issue":"2","key":"4_CR2","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."},{"key":"4_CR3","unstructured":"ArduPilot: Ardupilot - versatile, trusted, open (2024). https:\/\/www.ardupilot.org\/"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-319-96145-3_23","volume-title":"Computer Aided Verification","author":"G Argyros","year":"2018","unstructured":"Argyros, G., D\u2019Antoni, L.: The learnability of symbolic automata. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 427\u2013445. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_23"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Argyros, G., Stais, I., Jana, S., Keromytis, A.D., Kiayias, A.: SFADiff: automated evasion attacks and fingerprinting using black-box differential automata learning. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201916, pp. 1690\u20131701. ACM (2016). https:\/\/doi.org\/10.1145\/2976749.2978383","DOI":"10.1145\/2976749.2978383"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Argyros, G., Stais, I., Kiayias, A., Keromytis, A.D.: Back in black: towards formal, black box analysis of sanitizers and filters. In: Proceedings of the 37th IEEE Symposium on Security and Privacy, S&P \u201916, pp. 91\u2013109. IEEE (2016). https:\/\/doi.org\/10.1109\/SP.2016.14","DOI":"10.1109\/SP.2016.14"},{"key":"4_CR7","unstructured":"Ba, J., B\u00f6hme, M., Mirzamomen, Z., Roychoudhury, A.: Stateful greybox fuzzing. In: Proceedings of the 31st USENIX Security Symposium, USENIX Security \u201922, pp. 3255\u20133272. USENIX (2022). https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/ba"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260\u2013264. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_25"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: Proceedings of the 24th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201903, pp. 196\u2013207. ACM (2003). https:\/\/doi.org\/10.1145\/781131.781153","DOI":"10.1145\/781131.781153"},{"key":"4_CR10","unstructured":"BooFuzz: A fork and successor of the sulley fuzzing framework (2024). https:\/\/github.com\/jtpereyda\/boofuzz"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Botin\u010dan, M., Babi\u0107, D.: Sigma*: symbolic learning of input-output specifications. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, pp. 443\u2013456. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429123","DOI":"10.1145\/2429069.2429123"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Chen, Y., Song, L., Xing, X., Xu, F., Wu, W.: Automated finite state machine extraction. In: ACM Workshop on Forming an Ecosystem Around Software Transformation, FEAST \u201919, pp. 9\u201315. ACM (2019). https:\/\/doi.org\/10.1145\/3338502.3359760","DOI":"10.1145\/3338502.3359760"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Chubachi, K., Hendrian, D., Yoshinaka, R., Shinohara, A.: Query learning algorithm for residual symbolic finite automata. In: Proceedings of the 10th International Symposium on Games, Automata, Logics, and Formal Verification, G and ALF \u201919, pp. 140\u2013153. Open Publishing Association (2019). https:\/\/doi.org\/10.4204\/EPTCS.305.10","DOI":"10.4204\/EPTCS.305.10"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201977, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201979, pp. 269\u2013282. ACM (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Dalla\u00a0Preda, M., Giacobazzi, R., Lakhotia, A., Mastroeni, I.: Abstract symbolic automata: mixed syntactic\/semantic similarity analysis of executables. In: Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201915, pp. 329\u2013341. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676986","DOI":"10.1145\/2676726.2676986"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Daniele, C., Andarzian, S.B., Poll, E.: Fuzzers for stateful systems: survey and research directions. ACM Comput. Surv. (CSUR) 56(9), 222:1\u2013222:23 (2024). https:\/\/doi.org\/10.1145\/3648468","DOI":"10.1145\/3648468"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, pp. 541\u2013553. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535849","DOI":"10.1145\/2535838.2535849"},{"key":"4_CR20","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":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-15769-1_15","volume-title":"Static Analysis","author":"I Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Small formulas for large programs: on-line constraint simplification in scalable static analysis. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 236\u2013252. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_15"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-662-54577-5_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Drews","year":"2017","unstructured":"Drews, S., D\u2019Antoni, L.: Learning symbolic automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 173\u2013189. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_10"},{"issue":"1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10703-015-0233-4","volume":"47","author":"L D\u2019Antoni","year":"2015","unstructured":"D\u2019Antoni, L., Veanes, M.: Extended symbolic finite automata and transducers. Formal Methods Syst. Des. 47(1), 93\u2013119 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0233-4","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-662-54577-5_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L D\u2019Antoni","year":"2017","unstructured":"D\u2019Antoni, L., Veanes, M.: Forward bisimulations for nondeterministic symbolic finite automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 518\u2013534. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_30"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Garcia-Contreras, I., Govind, V.K.H., Shoham, S., Gurfinkel, A.: Fast approximations of quantifier elimination. In: Enea, C., Lal, A. (eds.) Proceedings of the 35th International Conference on Computer Aided Verification, CAV \u201923. Lecture Notes in Computer Science, vol. 13965, pp. 64\u201386. Springer, Cham (2023).https:\/\/doi.org\/10.1007\/978-3-031-37703-7_4","DOI":"10.1007\/978-3-031-37703-7_4"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Between testing and verification: dynamic software model checking. In: Dependable Software Systems Engineering, pp. 99\u2013116. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-99","DOI":"10.3233\/978-1-61499-627-9-99"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_22"},{"issue":"47","key":"4_CR28","doi-asserted-by":"publisher","first-page":"4029","DOI":"10.1016\/j.tcs.2010.07.008","volume":"411","author":"O Grinchtein","year":"2010","unstructured":"Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theoret. Comput. Sci. 411(47), 4029\u20134054 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.07.008","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-15769-1_18","volume-title":"Static Analysis","author":"A Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Boxes: a symbolic abstract domain of boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 287\u2013303. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_18"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69\u201385. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_7"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201902, pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"4_CR33","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with $$\\{$$BEK$$\\}$$. In: Proceedings of the 20th USENIX Security Symposium, USENIX Security \u201911, pp. 1\u201316. USENIX (2011). https:\/\/www.usenix.org\/conference\/usenix-security-11\/fast-and-precise-sanitizer-analysis-bek"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-18275-4_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Howar","year":"2011","unstructured":"Howar, F., Steffen, B., Merten, M.: Automata learning with automated alphabet abstraction refinement. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 263\u2013277. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_19"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-38088-4_9","volume-title":"NASA Formal Methods","author":"M Isberner","year":"2013","unstructured":"Isberner, M., Howar, F., Steffen, B.: Inferring automata with state-local alphabet abstractions. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 124\u2013138. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_9"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. (CSUR) 41(4), 21:1\u201321:54 (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Keil, M., Thiemann, P.: Symbolic solving of extended regular expression inequalities. In: Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS \u201914, pp. 175\u2013186. LIPIcs (2014). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2014.175","DOI":"10.4230\/LIPIcs.FSTTCS.2014.175"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Kim, K., et al.: FuzzUSB: hybrid stateful fuzzing of USB gadget stacks. In: IEEE Symposium on Security and Privacy, S&P \u201922, pp. 2212\u20132229. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833593","DOI":"10.1109\/SP46214.2022.9833593"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2nd International Symposium on Code Generation and Optimization, CGO \u201904, pp. 75:1\u201375:12. IEEE (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"4_CR40","doi-asserted-by":"publisher","first-page":"2673","DOI":"10.1109\/TIFS.2022.3192991","volume":"17","author":"J Li","year":"2022","unstructured":"Li, J., Li, S., Sun, G., Chen, T., Yu, H.: SNPSFuzzer: a fast greybox fuzzer for stateful network protocols using snapshots. IEEE Trans. Inf. Forensics Secur. 17, 2673\u20132687 (2022). https:\/\/doi.org\/10.1109\/TIFS.2022.3192991","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Li, L., Cifuentes, C., Keynes, N.: Boosting the performance of flow-sensitive points-to analysis using value flow. In: Proceedings of the 13th European Software Engineering Conference Held Jointly with the 19th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, ESEC\/FSE \u201911, pp. 343\u2013353. ACM (2011). https:\/\/doi.org\/10.1145\/2025113.2025160","DOI":"10.1145\/2025113.2025160"},{"key":"4_CR42","unstructured":"LibKiss: Kiss protocol (keep it simple stupid) parsing library for amateur radio (2023). https:\/\/github.com\/memoryhole\/libkiss"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-63121-9_8","volume-title":"Models, Algorithms, Logics and Tools","author":"O Maler","year":"2017","unstructured":"Maler, O., Mens, I.-E.: A generic algorithm for learning symbolic automata from membership queries. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 146\u2013169. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_8"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5\u201320. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_2"},{"key":"4_CR45","unstructured":"MAVLink: Mavlink developer guide (2024). https:\/\/mavlink.io\/en\/"},{"issue":"3","key":"4_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(3:13)2015","volume":"11","author":"IE Mens","year":"2015","unstructured":"Mens, I.E., Maler, O.: Learning regular languages over large ordered alphabets. Logical Methods Comput. Sci. 11(3), 1\u201322 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:13)2015","journal-title":"Logical Methods Comput. Sci."},{"key":"4_CR47","unstructured":"MIDI: A c library for parsing midi messages (2020). https:\/\/github.com\/binarynate\/midi-message-parser"},{"issue":"1","key":"4_CR48","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-order Symbolic Comput. 19(1), 31\u2013100 (2006). https:\/\/doi.org\/10.1007\/s10990-006-8609-1","journal-title":"Higher-order Symbolic Comput."},{"key":"4_CR49","unstructured":"Octave: Octave resource protocol guides (2022). https:\/\/docs.octave.dev\/docs\/octave-resource-protocol-guides"},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Ohmann, P., Brooks, A., D\u2019Antoni, L., Liblit, B.: Control-flow recovery from partial failure reports. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201917, pp. 390\u2013405. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062368","DOI":"10.1145\/3062341.3062368"},{"key":"4_CR51","unstructured":"PGFuzz: Policy-guided fuzzing for robotic vehicles (2023). https:\/\/github.com\/purseclab\/pgfuzz"},{"issue":"5","key":"4_CR52","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. (TOPLAS) 29(5), 26\u201377 (2007). https:\/\/doi.org\/10.1145\/1275497.1275501","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"4_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1007\/978-3-030-30942-8_37","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Sheinvald","year":"2019","unstructured":"Sheinvald, S.: Learning deterministic variable automata over infinite alphabets. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 633\u2013650. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_37"},{"key":"4_CR54","doi-asserted-by":"publisher","unstructured":"Shimizu, T., Yoshida, N., Yamamoto, R., Takada, H.: Symbolic execution-based approach to extracting a micro state transition table. In: ACM SIGSOFT International Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things, TAV-CPS\/IoT \u201919, pp. 1\u20136. ACM (2019). https:\/\/doi.org\/10.1145\/3341108.3342244","DOI":"10.1145\/3341108.3342244"},{"key":"4_CR55","unstructured":"SML: Smart message language parser (2023). https:\/\/github.com\/olliiiver\/sml_parser"},{"key":"4_CR56","doi-asserted-by":"publisher","unstructured":"Sotoudeh, M.: Automated verification of monotonic data structure traversals in C. In: Piskac, R., Rakamari\u0107, Z. (eds.) Proceedings of the 37th International Conference on Computer Aided Verification, CAV \u201925, pp. 29\u201355. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_2","DOI":"10.1007\/978-3-031-98668-0_2"},{"key":"4_CR57","doi-asserted-by":"publisher","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Software Eng. SE-12(1), 157\u2013171 (1986). https:\/\/doi.org\/10.1109\/TSE.1986.6312929","DOI":"10.1109\/TSE.1986.6312929"},{"key":"4_CR58","unstructured":"TinyFrame: A simple library for building and parsing data frames for serial interfaces (like uart \/ rs232) (2021). https:\/\/github.com\/mightypork\/tinyframe"},{"key":"4_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","volume-title":"Implementation and Application of Automata","author":"M Veanes","year":"2013","unstructured":"Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 16\u201323. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39274-0_3"},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-16242-8_45","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Veanes","year":"2010","unstructured":"Veanes, M., Bj\u00f8rner, N., de Moura, L.: Symbolic automata constraint solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 640\u2013654. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_45"},{"issue":"2","key":"4_CR61","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3040488","volume":"64","author":"M Veanes","year":"2017","unstructured":"Veanes, M., Bj\u00f8rner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. J. ACM 64(2), 1\u201328 (2017). https:\/\/doi.org\/10.1145\/3040488","journal-title":"J. ACM"},{"key":"4_CR62","doi-asserted-by":"publisher","unstructured":"Veanes, M., De\u00a0Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: Proceedings of the 3rd International Conference on Software Testing, Verification and Validation, ICST \u201910, pp. 498\u2013507. IEEE (2010). https:\/\/doi.org\/10.1109\/ICST.2010.15","DOI":"10.1109\/ICST.2010.15"},{"issue":"4","key":"4_CR63","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1017\/S135132499700154X","volume":"2","author":"BW Watson","year":"1996","unstructured":"Watson, B.W.: Implementing and using finite automata toolkits. Nat. Lang. Eng. 2(4), 295\u2013302 (1996). https:\/\/doi.org\/10.1017\/S135132499700154X","journal-title":"Nat. Lang. Eng."},{"key":"4_CR64","doi-asserted-by":"publisher","unstructured":"Xie, X., Chen, B., Liu, Y., Le, W., Li, X.: Proteus: Computing disjunctive loop summary via path dependency analysis. In: Proceedings of the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, FSE \u201916, pp. 61\u201372. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950340","DOI":"10.1145\/2950290.2950340"},{"issue":"6","key":"4_CR65","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1109\/TSE.2017.2788018","volume":"45","author":"X Xie","year":"2019","unstructured":"Xie, X., Chen, B., Zou, L., Liu, Y., Le, W., Li, X.: Automatic loop summarization via path dependency analysis. IEEE Trans. Software Eng. 45(6), 537\u2013557 (2019). https:\/\/doi.org\/10.1109\/TSE.2017.2788018","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR66","doi-asserted-by":"publisher","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201905, pp. 351\u2013363. ACM (2005). https:\/\/doi.org\/10.1145\/1040305.1040334","DOI":"10.1145\/1040305.1040334"},{"key":"4_CR67","doi-asserted-by":"publisher","unstructured":"Yao, P., Shi, Q., Huang, H., Zhang, C.: Program analysis via efficient symbolic abstraction. Proc. ACM Program. Lang. 5(OOPSLA), 118:1\u2013118:32 (2021). https:\/\/doi.org\/10.1145\/3485495","DOI":"10.1145\/3485495"},{"key":"4_CR68","unstructured":"Yaseen, N., Arzani, B., Beckett, R., Ciraci, S., Liu, V.: Aragog: scalable runtime verification of shardable networked systems. In: Proceedings of 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI \u201920, pp. 701\u2013718. USENIX (2020). https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/yaseen"},{"key":"4_CR69","doi-asserted-by":"publisher","unstructured":"Zhou, Z., Ye, Q., Delaware, B., Jagannathan, S.: A hat trick: automatically verifying representation invariants using symbolic finite automata. Proc. ACM Program. Lang. 8(PLDI), 203:1\u2013203:25 (2024). https:\/\/doi.org\/10.1145\/3656433","DOI":"10.1145\/3656433"}],"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-32537-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:18Z","timestamp":1784796258000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_4","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":"A public version of our tool is available at\n                      \n                      .","order":2,"name":"Ethics","label":"Data-Availability Statement","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"}}]}}