{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T15:28:43Z","timestamp":1773156523374,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2022,1,5]],"date-time":"2022-01-05T00:00:00Z","timestamp":1641340800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,5]],"date-time":"2022-01-05T00:00:00Z","timestamp":1641340800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10703-021-00385-1","type":"journal-article","created":{"date-parts":[[2022,1,5]],"date-time":"2022-01-05T19:06:43Z","timestamp":1641409603000},"page":"50-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Distributed bounded model checking"],"prefix":"10.1007","volume":"64","author":[{"given":"Prantik","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bui Phi","family":"Diep","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akash","family":"Lal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,1,5]]},"reference":[{"key":"385_CR1","doi-asserted-by":"crossref","unstructured":"Aiken A, Bugrara S, Dillig I, Dillig T, Hackett B, Hawkins P (2007) An overview of the Saturn project. In: Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp 43\u201348","DOI":"10.1145\/1251535.1251543"},{"issue":"6","key":"385_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/2345156.2254091","volume":"47","author":"A Albarghouthi","year":"2012","unstructured":"Albarghouthi A, Kumar R, Nori AV, Rajamani SK (2012) Parallelizing top-down interprocedural analyses. ACM SIGPLAN Not 47(6):217\u2013228","journal-title":"ACM SIGPLAN Not"},{"key":"385_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Bounimova E, Levin V, Kumar R, Lichtenberg J (2010) The static driver verifier research platform. In: Computer aided verification. Springer, pp 119\u2013122","DOI":"10.1007\/978-3-642-14295-6_11"},{"issue":"7","key":"385_CR4","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball T, Levin V, Rajamani SK (2011) A decade of software model checking with slam. Commun ACM 54(7):68\u201376","journal-title":"Commun ACM"},{"key":"385_CR5","doi-asserted-by":"crossref","unstructured":"Banga P, Pai A, Roy S, Chaudhuri M (2016) Accelerating schedule space exploration of multi-threaded programs with GPUs. In: Proceedings of the 14th ACM-IEEE international conference on formal methods and models for system design, MEMOCODE 16. IEEE Press, pp 115\u2013124","DOI":"10.1109\/MEMCOD.2016.7797754"},{"key":"385_CR6","unstructured":"Barnett M, Leino KRM, Moskal M, Schulte W (2009) Boogie: an intermediate verification language. https:\/\/github.com\/boogie-org\/boogie\/"},{"key":"385_CR7","doi-asserted-by":"crossref","unstructured":"Beyer D (2019) Automatic verification of C and Java programs: SV-COMP 2019. In: Tools and algorithms for the construction and analysis of systems\u201425 years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, pp 133\u2013155","DOI":"10.1007\/978-3-030-17502-3_9"},{"key":"385_CR8","doi-asserted-by":"crossref","unstructured":"Blicha M, Hyv\u00e4rinen AEJ, Marescotti M, Sharygina N (2020) A cooperative parallelization approach for property-directed k-induction. In: Beyer D, Zufferey D (eds) Verification, Model Checking, and Abstract Interpretation. Springer, Cham, pp 270\u2013292","DOI":"10.1007\/978-3-030-39322-9_13"},{"issue":"2","key":"385_CR9","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M B\u00f6hm","year":"1996","unstructured":"B\u00f6hm M, Speckenmeyer E (1996) A fast parallel SAT-solver\u2014efficient workload balancing. Ann Math Artif Intell 17(2):381\u2013400. https:\/\/doi.org\/10.1007\/BF02127976","journal-title":"Ann Math Artif Intell"},{"key":"385_CR10","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: Proceedings of the 12th international conference on verification, model checking, and abstract interpretation, VMCAI11. Springer-Verlag, pp 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"385_CR11","doi-asserted-by":"crossref","unstructured":"Carter M, He S, Whitaker J, Rakamaric Z, Emmi M (2016) Smack software verification toolchain. In: 2016 IEEE\/ACM 38th international conference on software engineering companion (ICSE-C). IEEE, pp 589\u2013592","DOI":"10.1145\/2889160.2889163"},{"key":"385_CR12","doi-asserted-by":"crossref","unstructured":"Chaki S, Karimi D (2016) Model checking with multi-threaded IC3 portfolios. In: Jobstmann B, Leino KRM (eds) Verification, Model Checking, and Abstract Interpretation. Springer, pp 517\u2013535","DOI":"10.1007\/978-3-662-49122-5_25"},{"key":"385_CR13","unstructured":"Chatterjee P, Roy S, Diep BP, Lal A (2020) Distributed bounded model checking. In: 2020 Formal methods in computer aided design (FMCAD). IEEE, pp 47\u201356"},{"key":"385_CR14","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Yorav K (2003) Behavioral consistency of C and Verilog programs using Bounded Model Checking. In: Proceedings of the 40th Design Automation Conference, DAC 2003, Anaheim, CA, USA, June 2\u20136, 2003, pp 368\u2013371","DOI":"10.1145\/775832.775928"},{"key":"385_CR15","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner N (2008) Z3: An efficient smt solver. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"385_CR16","doi-asserted-by":"publisher","unstructured":"Dureja R, Baumgartner J, Ivrii A, Kanzelman R, Rozier KY (2019) Boosting verification scalability via structural grouping and semantic partitioning of properties. In: 2019 Formal Methods in computer aided design (FMCAD), pp 1\u20139. https:\/\/doi.org\/10.23919\/FMCAD.2019.8894265","DOI":"10.23919\/FMCAD.2019.8894265"},{"key":"385_CR17","doi-asserted-by":"publisher","unstructured":"Dureja R, Baumgartner J, Kanzelman R, Williams M, Rozier KY (2020) Accelerating parallel verification via complementary property partitioning and strategy exploration. In: 2020 Formal methods in computer aided design (FMCAD), pp 16\u201325. https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_8","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_8"},{"key":"385_CR18","unstructured":"Een N, Mishchenko A, Brayton R (2011) Efficient implementation of property directed reachability. In: Proceedings of the international conference on formal methods in computer-aided design, FMCAD 11. FMCAD Inc, pp 125\u2013134"},{"key":"385_CR19","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2004) An extensible SAT-solver. In: Giunchiglia E, Tacchella A (eds) Theory and Applications of Satisfiability Testing. Springer, pp 502\u2013518","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"385_CR20","doi-asserted-by":"crossref","unstructured":"Ganai MK, Li W (2008) D-TSR: Parallelizing SMT-Based BMC using tunnels over a distributed framework. In: Haifa verification conference. Springer, pp 194\u2013199","DOI":"10.1007\/978-3-642-01702-5_19"},{"key":"385_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.4204\/eptcs.72.5","volume":"72","author":"Y Hamadi","year":"2011","unstructured":"Hamadi Y, Marques-Silva J, Wintersteiger CM (2011) Lazy decomposition for distributed decision procedures. Electron Proc Theor Comput Sci 72:43\u201354. https:\/\/doi.org\/10.4204\/eptcs.72.5","journal-title":"Electron Proc Theor Comput Sci"},{"key":"385_CR22","doi-asserted-by":"crossref","unstructured":"Hyv\u00e4rinen AEJ, Junttila T, Niemel\u00e4 I (2008) Incorporating learning in grid-based randomized SAT solving. In: Dochev D, Pistore M, Traverso P (eds) Artificial intelligence: methodology, systems, and applications. Springer, pp 247\u2013261","DOI":"10.1007\/978-3-540-85776-1_21"},{"key":"385_CR23","doi-asserted-by":"crossref","unstructured":"Inverso O, Trubiani C (2020) Parallel and distributed bounded model checking of multi-threaded programs. In: Proceedings of the 25th ACM SIGPLAN symposium on principles and practice of parallel programming, pp 202\u2013216","DOI":"10.1145\/3332466.3374529"},{"key":"385_CR24","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/S1571-0653(04)00321-X","volume":"9","author":"B Jurkowiak","year":"2001","unstructured":"Jurkowiak B, Li CM, Utard G (2001) Parallelizing Satz using dynamic workload balancing. Electron Not Discret Math 9:174\u2013189. https:\/\/doi.org\/10.1016\/S1571-0653(04)00321-X","journal-title":"Electron Not Discret Math"},{"key":"385_CR25","doi-asserted-by":"publisher","unstructured":"Kahsai T, Tinelli C (2011) PKIND: A parallel k-induction based model checker. EPTCS 72. https:\/\/doi.org\/10.4204\/EPTCS.72.6","DOI":"10.4204\/EPTCS.72.6"},{"key":"385_CR26","doi-asserted-by":"crossref","unstructured":"Kroening D, Tautschnig M (2014) Cbmc\u2013c bounded model checker. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 389\u2013391","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"385_CR27","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Qadeer S (2008) Back to the future: revisiting precise program verification using SMT solvers. In: POPL 08: Proceedings 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, pp 171\u2013182","DOI":"10.1145\/1328438.1328461"},{"key":"385_CR28","doi-asserted-by":"crossref","unstructured":"Lal A, Qadeer S (2013) Reachability modulo theories. In: Proceedings of Reachability problems\u20147th international workshop, RP 2013, Uppsala, Sweden, September 24\u201326, 2013, pp 23\u201344","DOI":"10.1007\/978-3-642-41036-9_4"},{"key":"385_CR29","doi-asserted-by":"crossref","unstructured":"Lal A, Qadeer S (2014) Powering the static driver verifier using corral. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, (FSE-22), Hong Kong, China, November 16\u201322, 2014, pp 202\u2013212","DOI":"10.1145\/2635868.2635894"},{"key":"385_CR30","doi-asserted-by":"crossref","unstructured":"Lal A, Qadeer S, Lahiri SK (2012) A solver for reachability modulo theories. In: Proceedings of computer aided verification\u201424th international conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, pp 427\u2013443. https:\/\/github.com\/boogie-org\/corral\/","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"385_CR31","doi-asserted-by":"crossref","unstructured":"Marescotti M, Gurfinkel A, Hyv\u00e4rinen AEJ, Sharygina N (2017) Designing parallel PDR. In: Proceedings of the 17th conference on formal methods in computer-aided design, FMCAD 17. FMCAD Inc, pp 156\u2013163","DOI":"10.23919\/FMCAD.2017.8102254"},{"key":"385_CR32","doi-asserted-by":"publisher","unstructured":"Marescotti M, Hyv\u00e4rinen A, Sharygina N (2018) SMTS: distributed, visualized constraint solving. In: Barthe G, Sutcliffe G, Veanes M (eds) LPAR-22. 22nd International conference on logic for programming, artificial intelligence and reasoning, EPiC series in computing, vol 57, pp 534\u2013542. EasyChair. https:\/\/doi.org\/10.29007\/fhgn. https:\/\/easychair.org\/publications\/paper\/k7BQ","DOI":"10.29007\/fhgn"},{"key":"385_CR33","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1109\/ICTAI.2010.56","volume":"1","author":"R Martins","year":"2010","unstructured":"Martins R, Manquinho V, Lynce I (2010) Improving search space splitting for parallel SAT solving. 2010 22nd IEEE International Conference on Tools with Artificial Intelligence 1:336\u2013343. https:\/\/doi.org\/10.1109\/ICTAI.2010.56","journal-title":"2010 22nd IEEE International Conference on Tools with Artificial Intelligence"},{"key":"385_CR34","unstructured":"Microsoft (2004) Static driver verifier. http:\/\/msdn.microsoft.com\/en-us\/library\/windows\/hardware\/ff552808(v=vs.85).aspx"},{"key":"385_CR35","unstructured":"Microsoft (2004) Static driver verifier benchmarks. https:\/\/github.com\/boogie-org\/sdvbench"},{"key":"385_CR36","doi-asserted-by":"crossref","unstructured":"Wintersteiger CM, Hamadi Y, Moura L (2009) A concurrent portfolio approach to SMT solving. In: Proceedings of the 21st international conference on computer aided verification, CAV 09. Springer, pp 715\u2013720","DOI":"10.1007\/978-3-642-02658-4_60"},{"issue":"4","key":"385_CR37","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang H, Bonacina MP, Hsiang J (1996) PSATO: a distributed propositional prover and its application to quasigroup problems. J Symbol Comput 21(4):543\u2013560. https:\/\/doi.org\/10.1006\/jsco.1996.0030","journal-title":"J Symbol Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00385-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00385-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00385-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:03:28Z","timestamp":1735409008000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00385-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,5]]},"references-count":37,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["385"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00385-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,5]]},"assertion":[{"value":"3 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 December 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 January 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}