{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:58:25Z","timestamp":1770292705141,"version":"3.49.0"},"publisher-location":"Cham","reference-count":67,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Identifying live and dead states in an abstract transition system is a recurring problem in formal verification; for example, it arises in our recent work on efficiently deciding regex constraints in SMT. However, state-of-the-art graph algorithms for maintaining reachability information<jats:italic>incrementally<\/jats:italic>(that is, as states are visited and before the entire state space is explored) assume that new edges can be added from any state at any time, whereas in many applications, outgoing edges are added from each state as it is explored. To formalize the latter situation, we propose<jats:italic>guided incremental digraphs<\/jats:italic>(GIDs), incremental graphs which support labeling<jats:italic>closed<\/jats:italic>states (states which will not receive further outgoing edges). Our main result is that dead state detection in GIDs is solvable in<jats:inline-formula><jats:tex-math>$$O(\\log m)$$<\/jats:tex-math><\/jats:inline-formula>amortized time per edge for<jats:italic>m<\/jats:italic>edges, improving upon<jats:inline-formula><jats:tex-math>$$O(\\sqrt{m})$$<\/jats:tex-math><\/jats:inline-formula>per edge due to Bender, Fineman, Gilbert, and Tarjan (BFGT) for general incremental directed graphs.<\/jats:p><jats:p>We introduce two algorithms for GIDs: one establishing the logarithmic time bound, and a second algorithm to explore a lazy heuristics-based approach. To enable an apples-to-apples experimental comparison, we implemented both algorithms, two simpler baselines, and the state-of-the-art BFGT baseline using a common directed graph interface in Rust. Our evaluation shows 110-530x speedups over BFGT for the largest input graphs over a range of graph classes, random graphs, and graphs arising from regex benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_12","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"241-264","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Incremental Dead State Detection in\u00a0Logarithmic Time"],"prefix":"10.1007","author":[{"given":"Caleb","family":"Stanford","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Abboud, A., Williams, V.V.: Popular conjectures imply strong lower bounds for dynamic problems. In: 2014 IEEE 55th Annual Symposium on Foundations of Computer Science, pp. 434\u2013443. IEEE (2014)","DOI":"10.1109\/FOCS.2014.53"},{"key":"12_CR2","unstructured":"Almeida, M., Moreira, N., Reis, R.: On the performance of automata minimization algorithms. Tech. Rep. DCC-2007-03, University of Porto (2007)"},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/1103963.1103966","volume":"1","author":"S Alstrup","year":"2005","unstructured":"Alstrup, S., Holm, J., Lichtenberg, K.D., Thorup, M.: Maintaining information in fully dynamic trees with top trees. Acm Trans. Algorithms (talg) 1(2), 243\u2013264 (2005)","journal-title":"Acm Trans. Algorithms (talg)"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3484198","volume":"55","author":"R Amadini","year":"2021","unstructured":"Amadini, R.: A survey on string constraint solving. ACM Comput. Surv. (CSUR) 55(1), 1\u201338 (2021)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"V Antimirov","year":"1995","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automata constructions. Theoret. Comput. Sci. 155, 291\u2013319 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR6","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 2018, Austin, TX, USA, 30 October - 2 November 2018, pp. 1\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"12_CR7","unstructured":"Bakaric, R.: Euler tour tree representation (GitHub repository) (2019). https:\/\/github.com\/RobertBakaric\/EulerTour"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Bender, M.A., Fineman, J.T., Gilbert, S., Tarjan, R.E.: A new approach to incremental cycle detection and related problems. ACM Trans. Algorithms 12(2), 14:1\u201314:22 (2015). https:\/\/doi.org\/10.1145\/2756553, https:\/\/arxiv.org\/abs\/1112.0784","DOI":"10.1145\/2756553"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Bernstein, A., Chechik, S.: Incremental topological sort and cycle detection in o(m sqrt(n)) expected total time. In: Proceedings of the 29th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2018, pp. 21\u201334. Society for Industrial and Applied Mathematics (2018)","DOI":"10.1137\/1.9781611975031.2"},{"key":"12_CR12","unstructured":"Berstel, J., Boasson, L., Carton, O., Fagnot, I.: Minimization of automata. Handbook of Automata (2011)"},{"key":"12_CR13","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":"12_CR14","doi-asserted-by":"crossref","unstructured":"Bhattacharya, S., Kulkarni, J.: An improved algorithm for incremental cycle detection and topological ordering in sparse graphs. In: Proceedings of the Fourteenth Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 2509\u20132521. SIAM (2020)","DOI":"10.1137\/1.9781611975994.153"},{"key":"12_CR15","unstructured":"Bj\u00f8rner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB format for sequences and regular expressions. In: SMT workshop, pp. 76\u201386 (2012), RegExLib benchmarks can be found at https:\/\/github.com\/cdstanford\/regex-smt-benchmarks\/, originally downloaded from https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/nbjorner-microsoft.automata.smtbenchmarks.zip"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(95)00199-9","volume":"57","author":"N Blum","year":"1996","unstructured":"Blum, N.: An $$O(n \\log n)$$ implementation of the standard method for minimizing $$n$$-state finite automata. Inf. Process. Lett. 57, 65\u201369 (1996)","journal-title":"Inf. Process. Lett."},{"key":"12_CR17","unstructured":"Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Proceedings of the Symposium on Mathematical Theory ofAutomata, New York, pp. 529\u2013561 (1963)"},{"issue":"4","key":"12_CR18","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":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-21254-3_13","volume-title":"Language and Automata Theory and Applications","author":"P Caron","year":"2011","unstructured":"Caron, P., Champarnaud, J.-M., Mignot, L.: Partial derivatives of an extended regular expression. In: Dediu, A.-H., Inenaga, S., Mart\u00edn-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 179\u2013191. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21254-3_13"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 415\u2013427. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_72"},{"key":"12_CR21","unstructured":"Cohen, E., Fiat, A., Kaplan, H., Roditty, L.: A Labeling Approach to Incremental Cycle Detection. arXiv preprint arXiv:1310.8381 (Oct 2013). https:\/\/arxiv.org\/abs\/1310.8381"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: ACM SIGPLAN Notices - POPL 2014, vol. 49(1), pp. 541\u2013553 (2014). https:\/\/doi.org\/10.1145\/2535838.2535849","DOI":"10.1145\/2535838.2535849"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13"},{"issue":"9","key":"12_CR24","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"issue":"4","key":"12_CR25","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)"},{"issue":"4","key":"12_CR26","first-page":"407","volume":"10","author":"K Ellul","year":"2005","unstructured":"Ellul, K., Krawetz, B., Shallit, J., Wang, M.W.: Regular expressions: New results and open problems. J. Autom. Lang. Comb. 10(4), 407\u2013437 (2005)","journal-title":"J. Autom. Lang. Comb."},{"key":"12_CR27","first-page":"1","volume":"1","author":"D Eppstein","year":"1999","unstructured":"Eppstein, D., Galil, Z., Italiano, G.F.: Dynamic graph algorithms. Algorithms Theory Comput. Handbook 1, 1\u20139 (1999)","journal-title":"Algorithms Theory Comput. Handbook"},{"key":"12_CR28","unstructured":"Fairbanks, J., Besan\u00e7on, M., Simon, S., Hoffiman, J., Eubank, N., Karpinski, S.: An optimized graphs package for the Julia programming language (2021). https:\/\/github.com\/JuliaGraphs\/Graphs.jl\/, commit 075a01eb6a"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Fan, W., Hu, C., Tian, C.: Incremental graph computations: Doable and undoable. In: Proceedings of the 2017 ACM International Conference on Management of Data, pp. 155\u2013169 (2017)","DOI":"10.1145\/3035918.3035944"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Frederickson, G.N.: A data structure for dynamically maintaining rooted trees. J. Algorithms 24(1), 37\u201365 (1997). https:\/\/arxiv.org\/pdf\/cs\/0310065.pdf","DOI":"10.1006\/jagm.1996.0835"},{"key":"12_CR31","unstructured":"Gelade, W., Neven, F.: Succinctness of the complement and intersection of regular expressions. arXiv preprint arXiv:0802.2869 (2008)"},{"key":"12_CR32","unstructured":"Gu\u00e9neau, A., Jourdan, J.H., Chargu\u00e9raud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Interactive Theorem Proving. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Haeupler, B., Kavitha, T., Mathew, R., Sen, S., Tarjan, R.E.: Incremental cycle detection, topological ordering, and strong component maintenance. ACM Trans. Algorithms 8(1.3), 1\u201333 ( 2012). https:\/\/doi.org\/10.1145\/2071379.2071382","DOI":"10.1145\/2071379.2071382"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Henzinger, M., King, V.: Fully dynamic biconnectivity and transitive closure. In: Proceedings of the 36th Annual Symposium on Foundations of Computer Science, pp. 664\u2013672, Milwaukee, WI (1995)","DOI":"10.1109\/SFCS.1995.492668"},{"issue":"4","key":"12_CR35","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1145\/320211.320215","volume":"46","author":"MR Henzinger","year":"1999","unstructured":"Henzinger, M.R., King, V.: Randomized fully dynamic graph algorithms with polylogarithmic time per operation. J. ACM (JACM) 46(4), 502\u2013516 (1999)","journal-title":"J. ACM (JACM)"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: Solving string constraints lazily. In: Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering, pp. 377\u2013386 (2010)","DOI":"10.1145\/1858996.1859080"},{"key":"12_CR37","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison Wesley (1979)"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $$n \\log n$$ algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations: Proceedings of an International Symposium on the Theory of Machines and Computations Held at Technion in Haifa, pp. 189\u2013196. Academic Press, New York (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"12_CR39","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., Boston (1969)"},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"Huffman, D.: The synthesis of sequential switching circuits. J. Franklin Inst. 257(3\u20134), 161\u2013190, 275\u2013303 (1954)","DOI":"10.1016\/0016-0032(54)90618-3"},{"key":"12_CR41","doi-asserted-by":"crossref","unstructured":"Kameda, T., Weiner, P.: On the state minimization of nondeterministic finite automata. IEEE Trans. Comput. C-19(7), 617\u2013627 (1970)","DOI":"10.1109\/T-C.1970.222994"},{"key":"12_CR42","unstructured":"Keil, M., Thiemann, P.: Symbolic solving of extended regular expression inequalities. In: FSTTCS 2014, pp. 175\u2013186. LIPIcs (2014)"},{"issue":"3","key":"12_CR43","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Design 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Design"},{"key":"12_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/3-540-45687-2_37","volume-title":"Mathematical Foundations of Computer Science 2002","author":"O Kupferman","year":"2002","unstructured":"Kupferman, O., Zuhovitzky, S.: An improved algorithm for the membership problem for extended regular expressions. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 446\u2013458. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45687-2_37"},{"key":"12_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-24246-0_9","volume-title":"Frontiers of Combining Systems","author":"T Liang","year":"2015","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 135\u2013150. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_9"},{"issue":"1","key":"12_CR46","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0020-0190(96)00075-0","volume":"59","author":"A Marchetti-Spaccamela","year":"1996","unstructured":"Marchetti-Spaccamela, A., Nanni, U., Rohnert, H.: Maintaining a topological order under edge insertions. Inf. Process. Lett. 59(1), 53\u201358 (1996). https:\/\/doi.org\/10.1016\/0020-0190(96)00075-0","journal-title":"Inf. Process. Lett."},{"key":"12_CR47","doi-asserted-by":"crossref","unstructured":"Matsakis, N.D., Klock, F.S.: The Rust language. ACM SIGAda Ada Letters 34(3), 103\u2013104 (2014). https:\/\/www.rust-lang.org\/","DOI":"10.1145\/2692956.2663188"},{"key":"12_CR48","doi-asserted-by":"crossref","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. In: POPL 2013, pp. 63\u201374 (2013)","DOI":"10.1145\/2480359.2429079"},{"key":"12_CR49","doi-asserted-by":"publisher","unstructured":"Mehlhorn, K.: Data Structures and Algorithms, Graph Algorithms and NP-Completeness, vol. 2. Springer (1984). https:\/\/doi.org\/10.1007\/978-3-642-69897-2","DOI":"10.1007\/978-3-642-69897-2"},{"key":"12_CR50","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines, pp. 129\u2013153. Automata studies, Annals of mathematics studies (1956)","DOI":"10.1515\/9781400882618-006"},{"key":"12_CR51","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":"12_CR52","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":"6","key":"12_CR53","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"12_CR54","unstructured":"Pearce, D.J.: Some directed graph algorithms and their application to pointer analysis. Ph.D. thesis, Imperial College, London (2005)"},{"key":"12_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-540-24838-5_29","volume-title":"Experimental and Efficient Algorithms","author":"DJ Pearce","year":"2004","unstructured":"Pearce, D.J., Kelly, P.H.J.: A dynamic algorithm for topologically sorting directed acyclic graphs. In: Ribeiro, C.C., Martins, S.L. (eds.) WEA 2004. LNCS, vol. 3059, pp. 383\u2013398. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24838-5_29"},{"key":"12_CR56","doi-asserted-by":"crossref","unstructured":"Pearce, D.J., Kelly, P.H.J.: A dynamic topological sort algorithm for directed acyclic graphs. ACM J. Experimental Algorithmics 11(1.7), 1\u201324 (2006)","DOI":"10.1145\/1187436.1210590"},{"issue":"5","key":"12_CR57","doi-asserted-by":"publisher","first-page":"1455","DOI":"10.1137\/060650271","volume":"37","author":"L Roditty","year":"2008","unstructured":"Roditty, L., Zwick, U.: Improved dynamic reachability algorithms for directed graphs. SIAM J. Comput. 37(5), 1455\u20131471 (2008). https:\/\/doi.org\/10.1137\/060650271","journal-title":"SIAM J. Comput."},{"key":"12_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"issue":"3","key":"12_CR59","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1016\/0022-0000(83)90006-5","volume":"26","author":"DD Sleator","year":"1983","unstructured":"Sleator, D.D., Tarjan, R.E.: A data structure for dynamic trees. J. Comput. Syst. Sci. 26(3), 362\u2013391 (1983)","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR60","doi-asserted-by":"crossref","unstructured":"Stanford, C., Veanes, M.: Incremental dead state detection in logarithmic time (extended version for arxiv). arXiv preprint arXiv:2301.05308 (2023)","DOI":"10.1007\/978-3-031-37703-7_12"},{"key":"12_CR61","doi-asserted-by":"crossref","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), pp. 620\u2013635 (2021)","DOI":"10.1145\/3453483.3454066"},{"key":"12_CR62","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Proceedings of the Fifth Annual ACM Symposium on Theory of Computing, pp. 1\u20139 (1973)","DOI":"10.1145\/800125.804029"},{"key":"12_CR63","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. JACM 22, 215\u2013225 (1975)","journal-title":"JACM"},{"key":"12_CR64","first-page":"4","volume":"14","author":"RE Tarjan","year":"2010","unstructured":"Tarjan, R.E., Werneck, R.F.: Dynamic trees in practice. J. Exp. Algorithmics (JEA) 14, 4\u20135 (2010)","journal-title":"J. Exp. Algorithmics (JEA)"},{"key":"12_CR65","unstructured":"Watson, B.W.: A taxonomy of finite automata minimization algorithms. Computing Science Report 93\/44, Eindhoven University of Technology (January 1995)"},{"issue":"1","key":"12_CR66","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1017\/S1351324903003127","volume":"9","author":"BW Watson","year":"2003","unstructured":"Watson, B.W., Daciuk, J.: An efficient incremental DFA minimization algorithm. Nat. Lang. Eng. 9(1), 49\u201364 (2003). https:\/\/doi.org\/10.1017\/S1351324903003127","journal-title":"Nat. Lang. Eng."},{"key":"12_CR67","doi-asserted-by":"crossref","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: egg: fast and extensible equality saturation. In: Proceedings of the ACM on Programming Languages 5(POPL), pp. 1\u201329 (2021)","DOI":"10.1145\/3434304"}],"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-031-37703-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T09:02:16Z","timestamp":1729760536000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_12","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":"18 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"26% - 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":"11","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)"}}]}}