{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:57Z","timestamp":1783545357736,"version":"3.55.0"},"publisher-location":"Cham","reference-count":32,"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>\n                    The integration of precise static analysis into interactive development environments (IDEs) necessitates algorithms that can update analysis results incrementally within milliseconds. However, maintaining\n                    <jats:italic>Bidirected Dyck-CFL reachability<\/jats:italic>\n                    \u2014the standard formalism for field-sensitive alias analysis\u2014under dynamic graph mutations remains an open challenge. Standard batch algorithms exhibit prohibiting cubic complexity (\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mathcal {O}(N^3)$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>O<\/mml:mi>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:msup>\n                              <mml:mi>N<\/mml:mi>\n                              <mml:mn>3<\/mml:mn>\n                            <\/mml:msup>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ), while existing dynamic approaches often lack formal guarantees when handling non-monotonic edge deletions (the \u201cghost path\u201d problem). In this paper, we present\n                    <jats:bold>GC-DBDR<\/jats:bold>\n                    , a novel incremental framework rooted in Abstract Interpretation. We reformulate the dynamic analysis problem not as graph patching, but as computing\n                    <jats:italic>Differential Fixpoints<\/jats:italic>\n                    over a lattice. By establishing a rigorous Galois Connection between execution traces and reachability relations, we derive update rules that are\n                    <jats:italic>correct-by-construction<\/jats:italic>\n                    . To resolve the asymmetry between monotonic insertions and non-monotonic deletions, we introduce a\n                    <jats:italic>Counting-Augmented Abstract Domain<\/jats:italic>\n                    supported by a\n                    <jats:italic>Derivation Hypergraph<\/jats:italic>\n                    . This structure operationalizes the\n                    <jats:italic>Inverse Abstraction Principle<\/jats:italic>\n                    , ensuring that reachability facts are retracted if and only if their supporting derivation trees are fully invalidated. We provide formal proofs demonstrating that GC-DBDR is sound and complete relative to batch analysis. Empirically, the algorithm achieves an optimal input-output complexity of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mathcal {O}(\\varDelta )$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>O<\/mml:mi>\n                            <mml:mo>(<\/mml:mo>\n                            <mml:mi>\u0394<\/mml:mi>\n                            <mml:mo>)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , delivering sub-millisecond tail latencies on real-world benchmarks.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_18","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:22:17Z","timestamp":1779024137000},"page":"347-366","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Correct-by-Construction Dynamic Reachability: A Galois-Connected Approach to\u00a0Bidirected Dyck Languages"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0772-8240","authenticated-orcid":false,"given":"Xiaofei","family":"Zhao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Blackburn, S.M., et al.: The dacapo benchmarks: java benchmarking development and analysis. https:\/\/doi.org\/10.1145\/1167473.1167488","DOI":"10.1145\/1167473.1167488"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications, pp. 128\u2013141. Springer Berlin Heidelberg","DOI":"10.1007\/BFb0039704"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Chaudhuri, S.: Subcubic algorithms for recursive state machines. https:\/\/doi.org\/10.1145\/1328438.1328460","DOI":"10.1145\/1328438.1328460"},{"key":"18_CR4","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. https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Demetrescu, C., Italiano, G.F.: Trade-offs for fully dynamic transitive closure on dags: breaking through the o(n2 barrier. J. ACM 52(2), 147\u2013156. https:\/\/doi.org\/10.1145\/1059513.1059514","DOI":"10.1145\/1059513.1059514"},{"issue":"8","key":"18_CR7","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/3338112","volume":"62","author":"D Distefano","year":"2019","unstructured":"Distefano, D., F\u00e4hndrich, M., Logozzo, F., O\u2019Hearn, P.W.: Scaling static analyses at facebook. Commun. ACM 62(8), 62\u201370 (2019)","journal-title":"Commun. ACM"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Doyle, J.: A truth maintenance system. Artif. Intell. 12(3), 231\u2013272. https:\/\/doi.org\/10.1016\/0004-3702(79)90008-0","DOI":"10.1016\/0004-3702(79)90008-0"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361\u2013416. https:\/\/doi.org\/10.1145\/333979.333989","DOI":"10.1145\/333979.333989"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361\u2013416. https:\/\/doi.org\/10.1145\/333979.333989","DOI":"10.1145\/333979.333989"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Hazimeh, A., Herrera, A., Payer, M.: Magma: a ground-truth fuzzing benchmark. Proc. ACM Meas. Anal. Comput. Syst. 4(3), Article 49. https:\/\/doi.org\/10.1145\/3428334","DOI":"10.1145\/3428334"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.J.: Incremental analysis of constraint logic programs. ACM Trans. Program. Lang. Syst. 22(2), 187\u2013223. https:\/\/doi.org\/10.1145\/349214.349216","DOI":"10.1145\/349214.349216"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.J.: Incremental analysis of constraint logic programs. ACM Trans. Program. Lang. Syst. 22(2), 187\u2013223. https:\/\/doi.org\/10.1145\/349214.349216","DOI":"10.1145\/349214.349216"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Johnson, B., Song, Y., Murphy-Hill, E., Bowdidge, R.: Why don\u2019t software developers use static analysis tools to find bugs? In: 2013 35th International Conference on Software Engineering (ICSE), pp. 672\u2013681. https:\/\/doi.org\/10.1109\/ICSE.2013.6606613","DOI":"10.1109\/ICSE.2013.6606613"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified c static analyzer. SIGPLAN Not. 50(1), 247\u2013259. https:\/\/doi.org\/10.1145\/2775051.2676966","DOI":"10.1145\/2775051.2676966"},{"key":"18_CR16","doi-asserted-by":"publisher","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), Article 42. https:\/\/doi.org\/10.1145\/3632884","DOI":"10.1145\/3632884"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Logozzo, F., Lahiri, S.K., F\u00e4hndrich, M., Blackshear, S.: Verification modulo versions: towards usable verification. SIGPLAN Not. 49(6), 294\u2013304. https:\/\/doi.org\/10.1145\/2666356.2594326","DOI":"10.1145\/2666356.2594326"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Mendez-Lojo, M., Burtscher, M., Pingali, K.: A GPU implementation of inclusion-based points-to analysis. SIGPLAN Not. 47(8), 107\u2013116. https:\/\/doi.org\/10.1145\/2370036.2145831","DOI":"10.1145\/2370036.2145831"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Nielsen, J.: Usability engineering. Morgan Kaufmann (1994)","DOI":"10.1016\/B978-0-08-052029-2.50009-7"},{"key":"18_CR20","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer Science & Business Media (2004)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Continuous reasoning: scaling the impact of formal methods. https:\/\/doi.org\/10.1145\/3209108.3209109","DOI":"10.1145\/3209108.3209109"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Ramalingam, G., Reps, T.: On the computational complexity of dynamic graph problems. Theor. Comput. Sci. 158(1), 233\u2013277. https:\/\/doi.org\/10.1016\/0304-3975(95)00079-8","DOI":"10.1016\/0304-3975(95)00079-8"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Reps, T.: Program analysis via graph reachability1an abbreviated version of this paper appeared as an invited paper in the proceedings of the 1997 international symposium on logic programming [84].1. Inf. Softw. Tech. 40(11), 701\u2013726. https:\/\/doi.org\/10.1016\/S0950-5849(98)00093-7","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Sridharan, M., Bod\u00edk, R.: Refinement-based context-sensitive points-to analysis for java. SIGPLAN Not. 41(6), 387\u2013400. https:\/\/doi.org\/10.1145\/1133255.1134027","DOI":"10.1145\/1133255.1134027"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. https:\/\/doi.org\/10.1145\/237721.237727","DOI":"10.1145\/237721.237727"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Szab\u00f3, T., Erdweg, S., Voelter, M.: Inca: a DSL for the definition of incremental program analyses. https:\/\/doi.org\/10.1145\/2970276.2970298","DOI":"10.1145\/2970276.2970298"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications (1955)","DOI":"10.2140\/pjm.1955.5.285"},{"key":"18_CR29","unstructured":"Vardi, M.Y.: Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems. ACM (1987)"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Yannakakis, M.: Graph-theoretic methods in database theory. https:\/\/doi.org\/10.1145\/298514.298576","DOI":"10.1145\/298514.298576"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Zhang, Q., Lyu, M.R., Yuan, H., Su, Z.: Fast algorithms for DYCK-CFL-reachability with applications to alias analysis. https:\/\/doi.org\/10.1145\/2491956.2462159","DOI":"10.1145\/2491956.2462159"},{"key":"18_CR32","doi-asserted-by":"publisher","unstructured":"Zheng, X., Rugina, R.: Demand-driven alias analysis for c. https:\/\/doi.org\/10.1145\/1328438.1328464","DOI":"10.1145\/1328438.1328464"}],"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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:30:14Z","timestamp":1783542614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_18","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"}}]}}