{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:52Z","timestamp":1750308592935,"version":"3.41.0"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,6]],"date-time":"2016-04-06T00:00:00Z","timestamp":1459900800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["15-08772S"],"award-info":[{"award-number":["15-08772S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2016,5,16]]},"abstract":"<jats:p>\n            Automatic verification of programs and computer systems with data nondeterminism (e.g., reading from user input) represents a significant and well-motivated challenge. The case of parallel programs is especially difficult, because then also the control flow nontrivially complicates the verification process. We apply the techniques of explicit-state model checking to account for the control aspects of a program to be verified and use\n            <jats:italic>set-based reduction<\/jats:italic>\n            of the data flow, thus handling the two sources of nondeterminism separately. We build the theory of set-based reduction using first-order formulae in the bit-vector theory to encode the sets of variable evaluations representing program data. These representations are tested for emptiness and equality (state matching) during the verification, and we harness modern satisfiability modulo theory solvers to implement these tests.\n          <\/jats:p>\n          <jats:p>We design two methods of implementing the state matching, one using quantifiers and one that is quantifier-free, and we provide both analytical and experimental comparisons. Further experiments evaluate the efficiency of the set-based reduction method, showing the classical, explicit approach to fail to scale with the size of data domains. Finally, we propose and evaluate two heuristics to decrease the number of expensive satisfiability queries, together yielding a 10-fold speedup.<\/jats:p>","DOI":"10.1145\/2888393","type":"journal-article","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T22:16:10Z","timestamp":1460067370000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Control Explicit--Data Symbolic Model Checking"],"prefix":"10.1145","volume":"25","author":[{"given":"Petr","family":"Bauch","sequence":"first","affiliation":[{"name":"Masaryk University, Brno, Botanicka, Czech Republic"}]},{"given":"Vojt\u011bch","family":"Havel","sequence":"additional","affiliation":[{"name":"Masaryk University, Brno, Botanicka, Czech Republic"}]},{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"additional","affiliation":[{"name":"Masaryk University, Brno, Botanicka, Czech Republic"}]}],"member":"320","published-online":{"date-parts":[[2016,4,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_10"},{"key":"e_1_2_1_2_1","volume-title":"Proc. of LICS. 88--98","author":"Andersen H.","year":"1997","unstructured":"H. Andersen and H. Hulgaard . 1997. Boolean expression diagrams . In Proc. of LICS. 88--98 . DOI:http:\/\/dx.doi. org\/10.1109\/LICS. 1997 .614938 H. Andersen and H. Hulgaard. 1997. Boolean expression diagrams. In Proc. of LICS. 88--98. DOI:http:\/\/dx.doi. org\/10.1109\/LICS.1997.614938"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2007.49"},{"key":"e_1_2_1_4_1","unstructured":"D. Babic and M. Musuvathi. 2005. Modular Arithmetic Decision Procedure. Technical Report. Microsoft Research Redmont.  D. Babic and M. Musuvathi. 2005. Modular Arithmetic Decision Procedure. Technical Report. Microsoft Research Redmont."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2014.44"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2014.20"},{"key":"e_1_2_1_7_1","volume-title":"FMICS. LNCS","volume":"7437","author":"Barnat J.","unstructured":"J. Barnat , J. Beran , L. Brim , T. Kratochv\u00edla , and P. Ro\u010dkai . 2012. Tool chain to support automated formal verification of avionics simulink designs . In FMICS. LNCS , Vol. 7437 . Springer, 78--92. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-32469-7_6 10.1007\/978-3-642-32469-7_6 J. Barnat, J. Beran, L. Brim, T. Kratochv\u00edla, and P. Ro\u010dkai. 2012. Tool chain to support automated formal verification of avionics simulink designs. In FMICS. LNCS, Vol. 7437. Springer, 78--92. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-32469-7_6"},{"key":"#cr-split#-e_1_2_1_8_1.1","doi-asserted-by":"crossref","unstructured":"J. Barnat L. Brim V. Havel J. Havl\u00ed\u010dek J. Kriho M. Len\u010do P. Ro\u010dkai V. \u0160till and J. Weiser. 2013. DiVinE 3.0 -- explicit-state model-checker for multithreaded C\/C++ programs. In CAV. 863--868. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-39799-8_60 10.1007\/978-3-642-39799-8_60","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"#cr-split#-e_1_2_1_8_1.2","doi-asserted-by":"crossref","unstructured":"J. Barnat L. Brim V. Havel J. Havl\u00ed\u010dek J. Kriho M. Len\u010do P. Ro\u010dkai V. \u0160till and J. Weiser. 2013. DiVinE 3.0 -- explicit-state model-checker for multithreaded C\/C++ programs. In CAV. 863--868. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-39799-8_60","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"e_1_2_1_9_1","volume-title":"SPIN. LNCS","volume":"2057","author":"Barnat J.","unstructured":"J. Barnat , L. Brim , and J. St\u0159\u00edbrn\u00e1 . 2001. Distributed LTL model-checking in SPIN . In SPIN. LNCS , Vol. 2057 . Springer, 200--216. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-45139-0_13 10.1007\/3-540-45139-0_13 J. Barnat, L. Brim, and J. St\u0159\u00edbrn\u00e1. 2001. Distributed LTL model-checking in SPIN. In SPIN. LNCS, Vol. 2057. Springer, 200--216. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-45139-0_13"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277186"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-014-9259-x"},{"key":"e_1_2_1_12_1","volume-title":"MEMICS. LNCS","volume":"8934","author":"Bauch P.","unstructured":"P. Bauch , V. Havel , and J. Barnat . 2014b. LTL model checking of LLVM bitcode with symbolic data . In MEMICS. LNCS , Vol. 8934 . Springer, 47--59. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-319-14896-0_5 10.1007\/978-3-319-14896-0_5 P. Bauch, V. Havel, and J. Barnat. 2014b. LTL model checking of LLVM bitcode with symbolic data. In MEMICS. LNCS, Vol. 8934. Springer, 47--59. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-319-14896-0_5"},{"key":"e_1_2_1_13_1","volume-title":"Proc. of ASP-DAC. 461--467","author":"Becker B.","year":"1997","unstructured":"B. Becker , R. Drechsler , and R. Enders . 1997. On the representational power of bit-level and word-level decision diagrams . In Proc. of ASP-DAC. 461--467 . DOI:http:\/\/dx.doi.org\/10.1109\/ASPDAC. 1997 .600304 10.1109\/ASPDAC.1997.600304 B. Becker, R. Drechsler, and R. Enders. 1997. On the representational power of bit-level and word-level decision diagrams. In Proc. of ASP-DAC. 461--467. DOI:http:\/\/dx.doi.org\/10.1109\/ASPDAC.1997.600304"},{"key":"#cr-split#-e_1_2_1_14_1.1","doi-asserted-by":"crossref","unstructured":"D. Beyer and M. Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In CAV. 184--190. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-22110-1_16 10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"#cr-split#-e_1_2_1_14_1.2","doi-asserted-by":"crossref","unstructured":"D. Beyer and M. Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In CAV. 184--190. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"e_1_2_1_16_1","volume-title":"TACAS. LNCS","volume":"1579","author":"Biere A.","unstructured":"A. Biere , A. Cimatti , E. Clarke , and Y. Zhu . 1999a. Symbolic model checking without BDDs . In TACAS. LNCS , Vol. 1579 . Springer, 193--207. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-49059-0_14 10.1007\/3-540-49059-0_14 A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. 1999a. Symbolic model checking without BDDs. In TACAS. LNCS, Vol. 1579. Springer, 193--207. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_17_1","volume-title":"Correct System Design. LNCS","volume":"1710","author":"Biere A.","unstructured":"A. Biere , E. Clarke , and Y. Zhu . 1999b. Multiple state and single state tableaux for combining local and global model checking . In Correct System Design. LNCS , Vol. 1710 . Springer, 163--179. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-48092-7_8 10.1007\/3-540-48092-7_8 A. Biere, E. Clarke, and Y. Zhu. 1999b. Multiple state and single state tableaux for combining local and global model checking. In Correct System Design. LNCS, Vol. 1710. Springer, 163--179. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-48092-7_8"},{"key":"e_1_2_1_19_1","volume-title":"FSTTCS. LNCS","volume":"1530","author":"Bohn J.","unstructured":"J. Bohn , W. Damm , O. Grumberg , H. Hungar , and K. Laster . 1998. First-order-CTL model checking . In FSTTCS. LNCS , Vol. 1530 . Springer, 283--294. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-49382-2_27 10.1007\/978-3-540-49382-2_27 J. Bohn, W. Damm, O. Grumberg, H. Hungar, and K. Laster. 1998. First-order-CTL model checking. In FSTTCS. LNCS, Vol. 1530. Springer, 283--294. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-49382-2_27"},{"key":"e_1_2_1_21_1","volume-title":"CAV. LNCS","volume":"818","author":"Boigelot B.","unstructured":"B. Boigelot and P. Wolper . 1994. Symbolic verification with periodic sets . In CAV. LNCS , Vol. 818 . Springer, 55--67. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-58179-0_43 10.1007\/3-540-58179-0_43 B. Boigelot and P. Wolper. 1994. Symbolic verification with periodic sets. In CAV. LNCS, Vol. 818. Springer, 55--67. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-58179-0_43"},{"key":"#cr-split#-e_1_2_1_22_1.1","doi-asserted-by":"crossref","unstructured":"A. Bradley. 2011. SAT-based model checking without unrolling. In VMCAI. 70--87. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-18275-4_7 10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"#cr-split#-e_1_2_1_22_1.2","doi-asserted-by":"crossref","unstructured":"A. Bradley. 2011. SAT-based model checking without unrolling. In VMCAI. 70--87. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"volume-title":"Proc. of Bytecode. Elsevier Science, 1--14","author":"Braione P.","key":"e_1_2_1_23_1","unstructured":"P. Braione , G. Denaro , B. K\u0159ena , and M. Pezz\u00e8 . 2008. Verifying LTL properties of bytecode with symbolic execution . In Proc. of Bytecode. Elsevier Science, 1--14 . P. Braione, G. Denaro, B. K\u0159ena, and M. Pezz\u00e8. 2008. Verifying LTL properties of bytecode with symbolic execution. In Proc. of Bytecode. Elsevier Science, 1--14."},{"volume-title":"FMCAD. LNCS","author":"Brim L.","key":"e_1_2_1_24_1","unstructured":"L. Brim , I. \u010cern\u00e1 , P. Moravec , and J. \u0160im\u0161a . 2004. Accepting predecessors are better than back edges in distributed LTL model-checking . In FMCAD. LNCS , Vol. 3312 . Springer , 352--366. DOI:http:\/\/dx.doi.org\/ 10.1007\/978-3-540-30494-4_25 10.1007\/978-3-540-30494-4_25 L. Brim, I. \u010cern\u00e1, P. Moravec, and J. \u0160im\u0161a. 2004. Accepting predecessors are better than back edges in distributed LTL model-checking. In FMCAD. LNCS, Vol. 3312. Springer, 352--366. DOI:http:\/\/dx.doi.org\/ 10.1007\/978-3-540-30494-4_25"},{"key":"e_1_2_1_25_1","volume-title":"CAV. LNCS","volume":"4590","author":"Bruttomesso R.","unstructured":"R. Bruttomesso , A. Cimatti , A. Franz\u00e9n , A. Griggio , Z. Hanna , A. Nadel , A. Palti , and R. Sebastiani . 2007. A lazy and layered SMT(BV) solver for hard industrial verification problems . In CAV. LNCS , Vol. 4590 . Springer, 547--560. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-73368-3_54 10.1007\/978-3-540-73368-3_54 R. Bruttomesso, A. Cimatti, A. Franz\u00e9n, A. Griggio, Z. Hanna, A. Nadel, A. Palti, and R. Sebastiani. 2007. A lazy and layered SMT(BV) solver for hard industrial verification problems. In CAV. LNCS, Vol. 4590. Springer, 547--560. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-73368-3_54"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217583"},{"key":"e_1_2_1_29_1","volume-title":"TACAS. LNCS","volume":"4424","author":"Bryant R.","unstructured":"R. Bryant , D. Kroening , J. Ouaknine , S. Seshia , O. Strichman , and B. Brady . 2007. Deciding bit-vector arithmetic with abstraction . In TACAS. LNCS , Vol. 4424 . Springer, 358--372. DOI:http:\/\/dx.doi.org\/ 10.1007\/978-3-540-71209-1_28 10.1007\/978-3-540-71209-1_28 R. Bryant, D. Kroening, J. Ouaknine, S. Seshia, O. Strichman, and B. Brady. 2007. Deciding bit-vector arithmetic with abstraction. In TACAS. LNCS, Vol. 4424. Springer, 358--372. DOI:http:\/\/dx.doi.org\/ 10.1007\/978-3-540-71209-1_28"},{"key":"e_1_2_1_30_1","volume-title":"ECOOP. LNCS","volume":"1357","author":"B\u00fcchi M.","unstructured":"M. B\u00fcchi and E. Sekerinski . 1998. Formal methods for component software: The refinement calculus perspective . In ECOOP. LNCS , Vol. 1357 . Springer, 332--337. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-69687-3_68 10.1007\/3-540-69687-3_68 M. B\u00fcchi and E. Sekerinski. 1998. Formal methods for component software: The refinement calculus perspective. In ECOOP. LNCS, Vol. 1357. Springer, 332--337. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-69687-3_68"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/271771.271799"},{"key":"e_1_2_1_32_1","volume-title":"SPIN. LNCS","volume":"2648","author":"\u010cern\u00e1 I.","unstructured":"I. \u010cern\u00e1 and R. Pel\u00e1nek . 2003. Distributed explicit fair cycle detection (set based approach) . In SPIN. LNCS , Vol. 2648 . Springer, 623--623. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-44829-2_4 10.1007\/3-540-44829-2_4 I. \u010cern\u00e1 and R. Pel\u00e1nek. 2003. Distributed explicit fair cycle detection (set based approach). In SPIN. LNCS, Vol. 2648. Springer, 623--623. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-44829-2_4"},{"key":"e_1_2_1_33_1","first-page":"173","article-title":"Canonical Graph-Based Representations for Verification of Arithmetic and Data Flow Designs. Cambridge University Press","volume":"7","author":"Ciesielski M.","year":"2009","unstructured":"M. Ciesielski , D. Pradhan , and A. Jabir . 2009 . Canonical Graph-Based Representations for Verification of Arithmetic and Data Flow Designs. Cambridge University Press , Chapter 7 , 173 -- 245 . M. Ciesielski, D. Pradhan, and A. Jabir. 2009. Canonical Graph-Based Representations for Verification of Arithmetic and Data Flow Designs. Cambridge University Press, Chapter 7, 173--245.","journal-title":"Chapter"},{"key":"e_1_2_1_34_1","first-page":"1","article-title":"Software model checking with explicit scheduler and symbolic threads","volume":"8","author":"Cimatti A.","year":"2012","unstructured":"A. Cimatti , I. Narasamdya , and M. Roveri . 2012 . Software model checking with explicit scheduler and symbolic threads . LMCS 8 , 2 (2012), 1 -- 42 . DOI:http:\/\/dx.doi.org\/10.2168\/LMCS-8(2:18)2012 10.2168\/LMCS-8(2:18)2012 A. Cimatti, I. Narasamdya, and M. Roveri. 2012. Software model checking with explicit scheduler and symbolic threads. LMCS 8, 2 (2012), 1--42. DOI:http:\/\/dx.doi.org\/10.2168\/LMCS-8(2:18)2012","journal-title":"LMCS"},{"key":"e_1_2_1_35_1","volume-title":"TACAS. LNCS","volume":"2031","author":"Cimatti A.","unstructured":"A. Cimatti , M. Roveri , and P. Bertoli . 2001. Searching powerset automata by combining explicit-state and symbolic model checking . In TACAS. LNCS , Vol. 2031 . Springer, 313--327. DOI:http:\/\/dx.doi.org\/ 10.1007\/3-540-45319-9_22 10.1007\/3-540-45319-9_22 A. Cimatti, M. Roveri, and P. Bertoli. 2001. Searching powerset automata by combining explicit-state and symbolic model checking. In TACAS. LNCS, Vol. 2031. Springer, 313--327. DOI:http:\/\/dx.doi.org\/ 10.1007\/3-540-45319-9_22"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_37_1","unstructured":"E. Clarke O. Grumberg and D. Peled. 1999. Model Checking. MIT Press.   E. Clarke O. Grumberg and D. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503230"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121128"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_42_1","volume-title":"CAV. LNCS","volume":"1254","author":"Cyrluk D.","unstructured":"D. Cyrluk , O. M\u00f6ller , and H. Rue\u00df . 1997. An efficient decision procedure for the theory of fixed-sized bit-vectors . In CAV. LNCS , Vol. 1254 . Springer, 60--71. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-63166-6_9 10.1007\/3-540-63166-6_9 D. Cyrluk, O. M\u00f6ller, and H. Rue\u00df. 1997. An efficient decision procedure for the theory of fixed-sized bit-vectors. In CAV. LNCS, Vol. 1254. Springer, 60--71. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-63166-6_9"},{"key":"e_1_2_1_43_1","volume-title":"TACAS. LNCS","volume":"4963","author":"de Moura L.","unstructured":"L. de Moura and N. Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In TACAS. LNCS , Vol. 4963 . Springer, 337--340. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24 L. de Moura and N. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In TACAS. LNCS, Vol. 4963. Springer, 337--340. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_44_1","volume-title":"CAV. LNCS","volume":"2725","author":"de Moura L.","unstructured":"L. de Moura , H. Rue\u00df , and M. Sorea . 2003. Bounded model checking and induction: From refutation to verification . In CAV. LNCS , Vol. 2725 . Springer, 14--26. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-45069-6_2 10.1007\/978-3-540-45069-6_2 L. de Moura, H. Rue\u00df, and M. Sorea. 2003. Bounded model checking and induction: From refutation to verification. In CAV. LNCS, Vol. 2725. Springer, 14--26. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-45069-6_2"},{"key":"e_1_2_1_45_1","volume-title":"ATVA. LNCS","volume":"6996","author":"Duret-Lutz A.","unstructured":"A. Duret-Lutz , K. Klai , D. Poitrenaud , and Y. Thierry-Mieg . 2011. Self-loop aggregation product\u2014A new hybrid approach to on-the-fly LTL model checking . In ATVA. LNCS , Vol. 6996 . Springer, 336--350. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-24372-1_24 10.1007\/978-3-642-24372-1_24 A. Duret-Lutz, K. Klai, D. Poitrenaud, and Y. Thierry-Mieg. 2011. Self-loop aggregation product\u2014A new hybrid approach to on-the-fly LTL model checking. In ATVA. LNCS, Vol. 6996. Springer, 336--350. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-24372-1_24"},{"key":"e_1_2_1_46_1","volume-title":"SPIN. LNCS","volume":"2318","author":"Eisner C.","unstructured":"C. Eisner and D. Peled . 2002. Comparing symbolic and explicit model checking of a software system . In SPIN. LNCS , Vol. 2318 . Springer, 230--239. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-46017-9_18 10.1007\/3-540-46017-9_18 C. Eisner and D. Peled. 2002. Comparing symbolic and explicit model checking of a software system. In SPIN. LNCS, Vol. 2318. Springer, 230--239. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-46017-9_18"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429086"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0059-8"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_2_1_50_1","volume-title":"ATVA. LNCS","volume":"3299","author":"Haddad S.","unstructured":"S. Haddad , J.-M. Ili\u00e9 , and K. Klai . 2004. Design and evaluation of a symbolic and abstraction-based model checker . In ATVA. LNCS , Vol. 3299 . Springer, 196--210. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-30476-0_19 10.1007\/978-3-540-30476-0_19 S. Haddad, J.-M. Ili\u00e9, and K. Klai. 2004. Design and evaluation of a symbolic and abstraction-based model checker. In ATVA. LNCS, Vol. 3299. Springer, 196--210. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-30476-0_19"},{"key":"e_1_2_1_51_1","volume-title":"Mona: Monadic second-order logic in practice. In TACAS. LNCS","author":"Henriksen J.","year":"1995","unstructured":"J. Henriksen , J. Jensen , M. J\u00f8rgensen , N. Klarlund , R. Paige , T. Rauhe , and A. Sandholm . 1995 . Mona: Monadic second-order logic in practice. In TACAS. LNCS , Vol. 1019 . Springer , 89--110. DOI:http:\/\/dx.doi.org\/ 10.1007\/3-540-60630-0_5 10.1007\/3-540-60630-0_5 J. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. 1995. Mona: Monadic second-order logic in practice. In TACAS. LNCS, Vol. 1019. Springer, 89--110. DOI:http:\/\/dx.doi.org\/ 10.1007\/3-540-60630-0_5"},{"key":"e_1_2_1_52_1","volume-title":"CHARME. LNCS","volume":"987","author":"Hungar H.","unstructured":"H. Hungar , O. Grumberg , and W. Damm . 1995. What if model checking must be truly symbolic . In CHARME. LNCS , Vol. 987 . Springer, 1--20. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-60385-9_1 10.1007\/3-540-60385-9_1 H. Hungar, O. Grumberg, and W. Damm. 1995. What if model checking must be truly symbolic. In CHARME. LNCS, Vol. 987. Springer, 1--20. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-60385-9_1"},{"key":"e_1_2_1_53_1","volume-title":"TACAS. LNCS","volume":"2619","author":"Khurshid S.","unstructured":"S. Khurshid , C. P\u0103s\u0103reanu , and W. Visser . 2003. Generalized symbolic execution for model checking and testing . In TACAS. LNCS , Vol. 2619 . Springer, 553--568. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-36577-X_40 10.1007\/3-540-36577-X_40 S. Khurshid, C. P\u0103s\u0103reanu, and W. Visser. 2003. Generalized symbolic execution for model checking and testing. In TACAS. LNCS, Vol. 2619. Springer, 553--568. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-36577-X_40"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_55_1","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kroening D.","year":"2010","unstructured":"D. Kroening and O. Strichman . 2010 . Decision Procedures: An Algorithmic Point of View . Springer . D. Kroening and O. Strichman. 2010. Decision Procedures: An Algorithmic Point of View. Springer."},{"key":"e_1_2_1_56_1","volume-title":"CAV. LNCS","volume":"1102","author":"Kupferman O.","unstructured":"O. Kupferman and M. Vardi . 1996. Module checking . In CAV. LNCS , Vol. 1102 . Springer, 75--86. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-61474-5_59 10.1007\/3-540-61474-5_59 O. Kupferman and M. Vardi. 1996. Module checking. In CAV. LNCS, Vol. 1102. Springer, 75--86. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-61474-5_59"},{"volume-title":"CONCUR. LNCS","author":"Lin H.","key":"e_1_2_1_57_1","unstructured":"H. Lin . 1996. Symbolic transition graph with assignment . In CONCUR. LNCS , Vol. 1119 . Springer , 50--65. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-61604-7_47 10.1007\/3-540-61604-7_47 H. Lin. 1996. Symbolic transition graph with assignment. In CONCUR. LNCS, Vol. 1119. Springer, 50--65. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-61604-7_47"},{"key":"e_1_2_1_58_1","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer.   Z. Manna and A. Pnueli. 1995. Temporal Verification of Reactive Systems: Safety. Springer.","DOI":"10.1007\/978-1-4612-4222-2"},{"volume-title":"CAV. LNCS","author":"McMillan K.","key":"e_1_2_1_60_1","unstructured":"K. McMillan . 2002. Applying SAT methods in unbounded symbolic model checking . In CAV. LNCS , Vol. 2404 . Springer , 250--264. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-45657-0_19 10.1007\/3-540-45657-0_19 K. McMillan. 2002. Applying SAT methods in unbounded symbolic model checking. In CAV. LNCS, Vol. 2404. Springer, 250--264. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-45657-0_19"},{"key":"#cr-split#-e_1_2_1_61_1.1","doi-asserted-by":"crossref","unstructured":"K. McMillan. 2003. Interpolation and SAT-based model checking. In CAV. 1--13. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-45069-6_1 10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"#cr-split#-e_1_2_1_61_1.2","doi-asserted-by":"crossref","unstructured":"K. McMillan. 2003. Interpolation and SAT-based model checking. In CAV. 1--13. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_62_1","volume-title":"BEEM: Benchmarks for explicit model checkers. In SPIN. LNCS","author":"Pel\u00e1nek R.","year":"2007","unstructured":"R. Pel\u00e1nek . 2007 . BEEM: Benchmarks for explicit model checkers. In SPIN. LNCS , Vol. 4595 . Springer , 263--267. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-73370-6_17 10.1007\/978-3-540-73370-6_17 R. Pel\u00e1nek. 2007. BEEM: Benchmarks for explicit model checkers. In SPIN. LNCS, Vol. 4595. Springer, 263--267. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-73370-6_17"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040317"},{"key":"e_1_2_1_65_1","volume-title":"FMCAD. LNCS","volume":"1166","author":"Ravi K.","unstructured":"K. Ravi , A. Pardo , G. Hachtel , and F. Somenzi . 1996. Modular verification of multipliers . In FMCAD. LNCS , Vol. 1166 . Springer, 49--63. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0031799 10.1007\/BFb0031799 K. Ravi, A. Pardo, G. Hachtel, and F. Somenzi. 1996. Modular verification of multipliers. In FMCAD. LNCS, Vol. 1166. Springer, 49--63. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0031799"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_35"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"volume-title":"CADE. LNCS","author":"Shostak R.","key":"e_1_2_1_68_1","unstructured":"R. Shostak . 1982. Deciding combinations of theories . In CADE. LNCS , Vol. 138 . Springer , 209--222. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0000061 10.1007\/BFb0000061 R. Shostak. 1982. Deciding combinations of theories. In CADE. LNCS, Vol. 138. Springer, 209--222. DOI:http:\/\/dx.doi.org\/10.1007\/BFb0000061"},{"volume-title":"DiVinE -- Distributed Verification Environment. Master\u2019s thesis","author":"\u0160ime\u010dek P.","key":"e_1_2_1_69_1","unstructured":"P. \u0160ime\u010dek . 2006. DiVinE -- Distributed Verification Environment. Master\u2019s thesis . Masaryk University . P. \u0160ime\u010dek. 2006. DiVinE -- Distributed Verification Environment. Master\u2019s thesis. Masaryk University."},{"key":"e_1_2_1_70_1","volume-title":"SAS. LNCS","volume":"4634","author":"Simon A.","unstructured":"A. Simon and A. King . 2007. Taming the wrapping of integer arithmetic . In SAS. LNCS , Vol. 4634 . Springer, 121--136. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-74061-2_8 10.1007\/978-3-540-74061-2_8 A. Simon and A. King. 2007. Taming the wrapping of integer arithmetic. In SAS. LNCS, Vol. 4634. Springer, 121--136. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-74061-2_8"},{"volume-title":"TACAS. LNCS","author":"Vardi M.","key":"e_1_2_1_71_1","unstructured":"M. Vardi . 2001. Branching vs. linear time: Final showdown . In TACAS. LNCS , Vol. 2031 . Springer , 1--22. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-45319-9_1 10.1007\/3-540-45319-9_1 M. Vardi. 2001. Branching vs. linear time: Final showdown. In TACAS. LNCS, Vol. 2031. Springer, 1--22. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-45319-9_1"},{"volume-title":"Proc. of LICS. IEEE Computer Society Press, 332--344","author":"Vardi M.","key":"e_1_2_1_72_1","unstructured":"M. Vardi and P. Wolper . 1986. An automata-theoretic approach to automatic program verification . In Proc. of LICS. IEEE Computer Society Press, 332--344 . M. Vardi and P. Wolper. 1986. An automata-theoretic approach to automatic program verification. In Proc. of LICS. IEEE Computer Society Press, 332--344."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_16"},{"key":"e_1_2_1_74_1","volume-title":"CAV. LNCS","volume":"1855","author":"Williams P.","unstructured":"P. Williams , A. Biere , E. Clarke , and A. Gupta . 2000. Combining decision diagrams and SAT procedures for efficient symbolic model checking . In CAV. LNCS , Vol. 1855 . Springer, 124--138. DOI:http:\/\/dx.doi.org\/ 10.1007\/10722167_13 10.1007\/10722167_13 P. Williams, A. Biere, E. Clarke, and A. Gupta. 2000. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In CAV. LNCS, Vol. 1855. Springer, 124--138. DOI:http:\/\/dx.doi.org\/ 10.1007\/10722167_13"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0156-2"},{"key":"e_1_2_1_76_1","first-page":"1","article-title":"On the construction of automata from linear arithmetic constraints","volume":"1785","author":"Wolper P.","year":"2000","unstructured":"P. Wolper and B. Boigelot . 2000 . On the construction of automata from linear arithmetic constraints . In TACAS. LNCS , Vol. 1785. 1 -- 19 . DOI:http:\/\/dx.doi.org\/10.1007\/3-540-46419-0_1 10.1007\/3-540-46419-0_1 P. Wolper and B. Boigelot. 2000. On the construction of automata from linear arithmetic constraints. In TACAS. LNCS, Vol. 1785. 1--19. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-46419-0_1","journal-title":"TACAS. LNCS"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_24"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2888393","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2888393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:25Z","timestamp":1750273525000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2888393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,6]]},"references-count":77,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,5,16]]}},"alternative-id":["10.1145\/2888393"],"URL":"https:\/\/doi.org\/10.1145\/2888393","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2016,4,6]]},"assertion":[{"value":"2015-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}