{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T14:06:36Z","timestamp":1779026796725,"version":"3.51.4"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","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,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"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>Static analysis plays a crucial role in program optimization, bug detection, and automated testing. Dyck-reachability provides a foundational formulation for static analysis, as Dyck grammars can model critical properties such as\u00a0field and context sensitivity, thus offering broad applicability. This paper shows that static analysis problems modeled as Dyck-reachability on bidirected graphs can be encoded into the EUF SMT theory; consequently, all such problems admit efficient formulation and solution via EUF-based SMT solvers. By leveraging the optimized nature of modern SMT solvers, our method achieves efficiency comparable to state-of-the-art graph-based bidirected Dyck-reachability algorithms\u00a0while eliminating the need for developing complex specialized graph reachability algorithms. Our approach opens new avenues for solving these classical static analysis problems, demonstrating the strong potential of SMT solvers in encoding static analysis solutions.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_15","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:57Z","timestamp":1779024117000},"page":"296-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["EUF-based Solving Dyck-Reachability with\u00a0Applications to\u00a0Static Analysis"],"prefix":"10.1007","author":[{"given":"Yide","family":"Du","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4066-7892","authenticated-orcid":false,"given":"Zhenbang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kunlin","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2359-9687","authenticated-orcid":false,"given":"Guofeng","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ke","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8033-7943","authenticated-orcid":false,"given":"Wei","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":false,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"15_CR1","unstructured":"sPECjvm2008 Benchmark Suit (2008). http:\/\/www.spec.org\/jvm2008\/"},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/BF01459088","volume":"99","author":"W Ackermann","year":"1928","unstructured":"Ackermann, W.: Zum hilbertschen aufbau der reellen zahlen. Math. Ann. 99(1), 118\u2013133 (1928)","journal-title":"Math. Ann."},{"issue":"3","key":"15_CR3","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/360018.360025","volume":"19","author":"FE Allen","year":"1976","unstructured":"Allen, F.E., Cocke, J.: A program data flow analysis procedure. Commun. ACM 19(3), 137 (1976)","journal-title":"Commun. ACM"},{"key":"15_CR4","unstructured":"Andersen, L.O.: Program analysis and specialization for the c programming language (1994)"},{"issue":"3","key":"15_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3182657","volume":"51","author":"R Baldoni","year":"2018","unstructured":"Baldoni, R., Coppa, E., D\u2019elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 1\u201339 (2018)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et\u00a0al.: cvc5: a versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"15_CR7","unstructured":"Barrett, C., et\u00a0al.: The SMT-lib standard: version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), Vol.\u00a013, p.\u00a014 (2010)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Blackburn, S.M., et\u00a0al.: The DaCapo benchmarks: java benchmarking development and analysis. In: Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-oriented Programming Systems, Languages, And Application, pp. 169\u2013190 (2006)","DOI":"10.1145\/1167473.1167488"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, M., Pham, V.T., Nguyen, M.D., Roychoudhury, A.: Directed greybox fuzzing. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 2329\u20132344 (2017)","DOI":"10.1145\/3133956.3134020"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Choudhary, B., Pavlogiannis, A.: Optimal Dyck reachability for data-dependence and alias analysis. Proc. ACM Program. Lang. 2(POPL), 1\u201330 (2017)","DOI":"10.1145\/3158118"},{"key":"15_CR11","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT press (2022)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"15_CR13","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM (JACM) 52(3), 365\u2013473 (2005)","journal-title":"J. ACM (JACM)"},{"key":"15_CR14","unstructured":"Lotus developers: lotus, program analysis and verification framework. https:\/\/github.com\/ZJU-Automated-Reasoning-Group\/lotus"},{"key":"15_CR15","unstructured":"Developers, S.: Souffl\u00e9, logic defined static analysis. https:\/\/souffle-lang.github.io\/"},{"issue":"4","key":"15_CR16","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM (JACM) 27(4), 758\u2013771 (1980)","journal-title":"J. ACM (JACM)"},{"key":"15_CR17","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.18871949","author":"Y Du","year":"2026","unstructured":"Du, Y., et al.: EUF-based solving DYCK-reachability with applications to static analysis (2026). https:\/\/doi.org\/10.5281\/zenodo.18871949","journal-title":"EUF-based solving DYCK-reachability with applications to static analysis"},{"key":"15_CR18","unstructured":"Dutertre, B., De\u00a0Moura, L.: The YICES SMT solver. Tool paper at 2(2), 1\u20132 (2006). http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"15_CR19","unstructured":"Ewert, D.: platsat (2024), toy \u2019QF_UF\u2019 SMT solver written in Rust. https:\/\/github.com\/dewert99\/plat-smt"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Habib, A., Pradel, M.: How many of all bugs do we find? A study of static bug detectors. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, pp. 317\u2013328 (2018)","DOI":"10.1145\/3238147.3238213"},{"key":"15_CR21","volume-title":"Formal languages and their relation to automata","author":"JE Hopcroft","year":"1969","unstructured":"Hopcroft, J.E., Ullman, J.D.: Formal languages and their relation to automata. Addison-Wesley Longman Publishing Co., Inc (1969)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Jin, D., Meredith, P.O., Lee, C., Ro\u015fu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 1427\u20131430. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Kjelstr\u00f8m, A.H., Pavlogiannis, A.: The decidability and complexity of interleaved bidirected DYCK reachability. Proc. ACM Program. Lang. 6(POPL), 1\u201326 (2022)","DOI":"10.1145\/3498673"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Koutris, P., Deep, S.: The fine-grained complexity of CFL reachability. Proc. ACM Program. Lang. 7(POPL), 1713\u20131739 (2023)","DOI":"10.1145\/3571252"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Krishna, S., Lal, A., Pavlogiannis, A., Tuppe, O.: On-the-fly static analysis via dynamic bidirected DYCK reachability. Proc. ACM Program. Lang. 8(POPL), 1239\u20131268 (2024)","DOI":"10.1145\/3632884"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Li, Y., Satya, K., Zhang, Q.: Efficient algorithms for dynamic bidirected DYCK-reachability. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022)","DOI":"10.1145\/3498724"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Li, Y., Zhang, Q., Reps, T.: On the complexity of bidirected interleaved DYCK-reachability. Proc. ACM Program. Lang. 5(POPL), 1\u201328 (2021)","DOI":"10.1145\/3434340"},{"issue":"2","key":"15_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3492428","volume":"44","author":"Y Li","year":"2022","unstructured":"Li, Y., Zhang, Q., Reps, T.: Fast graph simplification for interleaved-DYCK reachability. ACM Trans. Program. Lang. Syst. (TOPLAS) 44(2), 1\u201328 (2022)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Mathiasen, A.A., Pavlogiannis, A.: The fine-grained and parallel complexity of andersen\u2019s pointer analysis. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021)","DOI":"10.1145\/3434315"},{"issue":"2","key":"15_CR31","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. (TOPLAS) 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"2","key":"15_CR32","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM (JACM) 27(2), 356\u2013364 (1980)","journal-title":"J. ACM (JACM)"},{"issue":"4","key":"15_CR33","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"issue":"11\u201312","key":"15_CR34","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/S0950-5849(98)00093-7","volume":"40","author":"T Reps","year":"1998","unstructured":"Reps, T.: Program analysis via graph reachability. Inf. Softw. Technol. 40(11\u201312), 701\u2013726 (1998)","journal-title":"Inf. Softw. Technol."},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"issue":"5","key":"15_CR36","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/1095430.1081750","volume":"30","author":"K Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: A concolic unit testing engine for c. ACM SIGSOFT Softw. Eng. Notes 30(5), 263\u2013272 (2005)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Shi, Q., et al.: Pinpoint: fast and precise sparse value flow analysis for million lines of code. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 693\u2013706 (2018)","DOI":"10.1145\/3192366.3192418"},{"key":"15_CR38","unstructured":"SMT-COMP organizers: 2024 SMT competition results. Online Resource (2024). https:\/\/smt-comp.github.io\/2024\/results\/"},{"issue":"6","key":"15_CR39","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/1133255.1134027","volume":"41","author":"M Sridharan","year":"2006","unstructured":"Sridharan, M., Bod\u00edk, R.: Refinement-based context-sensitive points-to analysis for java. ACM SIGPLAN Notices 41(6), 387\u2013400 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR40","doi-asserted-by":"crossref","unstructured":"Tang, H., et al.: Summary-based context-sensitive data-dependence analysis in presence of callbacks. In: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 83\u201395 (2015)","DOI":"10.1145\/2676726.2676997"},{"key":"15_CR41","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, pp. 131\u2013144 (2004)","DOI":"10.1145\/996841.996859"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"Willsey, M., et al.: Egg: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021)","DOI":"10.1145\/3434304"},{"key":"15_CR43","doi-asserted-by":"crossref","unstructured":"Yan, D., Xu, G., Rountev, A.: Demand-driven context-sensitive alias analysis for java. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis, pp. 155\u2013165 (2011)","DOI":"10.1145\/2001420.2001440"},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Zhang, Q., Lyu, M.R., Yuan, H., Su, Z.: Fast algorithms for DYCK-CFL-reachability with applications to alias analysis. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 435\u2013446 (2013)","DOI":"10.1145\/2491956.2462159"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:22:03Z","timestamp":1779024123000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_15","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}