{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:52:48Z","timestamp":1742946768840,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030174644"},{"type":"electronic","value":"9783030174651"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17465-1_4","type":"book-chapter","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T02:50:37Z","timestamp":1554346237000},"page":"58-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Multi-core On-The-Fly Saturation"],"prefix":"10.1007","author":[{"given":"Tom","family":"van Dijk","sequence":"first","affiliation":[]},{"given":"Jeroen","family":"Meijer","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: FORCE: a fast and easy-to-implement variable-ordering heuristic. In: VLSI 2003, pp. 116\u2013119. ACM (2003)","DOI":"10.1145\/764808.764839"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-68167-2_13","volume-title":"Automated Technology for Verification and Analysis","author":"EG Amparore","year":"2017","unstructured":"Amparore, E.G., Beccuti, M., Donatelli, S.: Gradient-based variable ordering of decision diagrams for systems with structural units. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 184\u2013200. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_13"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Donatelli, S., Beccuti, M., Garbi, G., Miner, A.S.: Decision diagrams for Petri nets: which variable ordering? In: PNSE @ Petri Nets. CEUR Workshop Proceedings, vol. 1846, pp. 31\u201350. CEUR-WS.org (2017)","DOI":"10.1007\/978-3-662-58381-4_4"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Babar, J., Miner, A.S.: Meddly: multi-terminal and edge-valued decision diagram library. In: QEST, pp. 195\u2013196. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.34"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354\u2013359. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_31"},{"issue":"9","key":"4_CR6","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"issue":"8","key":"4_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C\u201335(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-319-89960-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2018","unstructured":"Bryant, R.E.: Chain reduction for binary and zero-suppressed decision diagrams. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 81\u201398. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_5"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Chung, M., Ciardo, G.: Saturation NOW. In: QEST, pp. 272\u2013281. IEEE Computer Society (2004)","DOI":"10.1109\/QEST.2004.1348041"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1093\/logcom\/exp005","volume":"21","author":"M Chung","year":"2011","unstructured":"Chung, M., Ciardo, G.: Speculative image computation for distributed symbolic reachability analysis. J. Logic Comput. 21(1), 63\u201383 (2011)","journal-title":"J. Logic Comput."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ciardo","year":"2001","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: an efficient iteration strategy for symbolic state\u2014space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328\u2013342. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_23"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/3-540-36577-X_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ciardo","year":"2003","unstructured":"Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379\u2013393. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_27"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. STTT 8(1), 4\u201325 (2006)","journal-title":"STTT"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Ciardo, G., Zhao, Y., Jin, X.: Parallel symbolic state-space exploration is difficult, but what is the alternative? In: PDMC, EPTCS, vol. 14, pp. 1\u201317 (2009)","DOI":"10.4204\/EPTCS.14.1"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"van Dijk, T.: Sylvan: multi-core decision diagrams. Ph.D. thesis, University of Twente, July 2016","DOI":"10.1007\/s10009-016-0433-2"},{"issue":"6","key":"4_CR16","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T Dijk van","year":"2017","unstructured":"van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. STTT 19(6), 675\u2013696 (2017)","journal-title":"STTT"},{"issue":"2","key":"4_CR17","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10009-017-0468-z","volume":"20","author":"T Dijk van","year":"2018","unstructured":"van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. STTT 20(2), 157\u2013177 (2018)","journal-title":"STTT"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-14313-2_18","volume-title":"Euro-Par 2014: Parallel Processing Workshops","author":"T Dijk van","year":"2014","unstructured":"van Dijk, T., van de Pol, J.C.: Lace: non-blocking split deque for work-stealing. In: Lopes, L., et al. (eds.) Euro-Par 2014. LNCS, vol. 8806, pp. 206\u2013217. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-14313-2_18"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"van Dijk, T., Wille, R., Meolic, R.: Tagged BDDs: combining reduction rules from different decision diagram types. In: FMCAD, pp. 108\u2013115. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102248"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-73368-3_31","volume-title":"Computer Aided Verification","author":"J Ezekiel","year":"2007","unstructured":"Ezekiel, J., L\u00fcttgen, G., Ciardo, G.: Parallelising symbolic state-space generators. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 268\u2013280. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_31"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1023\/A:1020373206491","volume":"21","author":"T Heyman","year":"2002","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: A scalable parallel algorithm for reachability analysis of very large circuits. Formal Methods Syst. Des. 21(3), 317\u2013338 (2002)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"4_CR23","unstructured":"Konnov, I., Letichevsky, O.: Model checking GARP protocol using Spin and VRS. In: IW on Automata, Algorithms, and Information Technology (2010)"},{"key":"4_CR24","unstructured":"Kordon, F., et al.: Complete Results for the 2016 Edition of the Model Checking Contest, June 2016. http:\/\/mcc.lip6.fr\/2016\/results.php"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-319-13338-6_16","volume-title":"Hardware and Software: Verification and Testing","author":"J Meijer","year":"2014","unstructured":"Meijer, J., Kant, G., Blom, S., van de Pol, J.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 204\u2013219. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_16"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-40648-0_20","volume-title":"NASA Formal Methods","author":"J Meijer","year":"2016","unstructured":"Meijer, J., van de Pol, J.: Bandwidth and wavefront reduction for static variable ordering in symbolic reachability analysis. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 255\u2013271. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_20"},{"key":"4_CR27","unstructured":"Noack, A.: A ZBDD package for efficient model checking of Petri nets. Forschungsbericht, Branderburgische Technische Uinversit\u00e4t Cottbus (1999)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Oortwijn, W., van Dijk, T., van de Pol, J.: Distributed binary decision diagrams for symbolic reachability. In: 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 21\u201330 (2017)","DOI":"10.1145\/3092282.3092284"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/11691372_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Siminiceanu","year":"2006","unstructured":"Siminiceanu, R., Ciardo, G.: New metrics for static variable ordering in decision diagrams. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 90\u2013104. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_6"},{"issue":"11","key":"4_CR30","doi-asserted-by":"publisher","first-page":"2651","DOI":"10.1002\/nme.1620281111","volume":"28","author":"SW Sloan","year":"1989","unstructured":"Sloan, S.W.: A FORTRAN program for profile and wavefront reduction. Int. J. Numer. Methods Eng. 28(11), 2651\u20132679 (1989)","journal-title":"Int. J. Numer. Methods Eng."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"V\u00f6r\u00f6s, A., Szab\u00f3, T., J\u00e1mbor, A., Darvas, D., Horv\u00e1th, \u00c1., Bartha, T.: Parallel saturation based model checking. In: ISPDC, pp. 94\u2013101. IEEE Computer Society (2011)","DOI":"10.1109\/ISPDC.2011.23"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-04761-9_27","volume-title":"Automated Technology for Verification and Analysis","author":"Y Zhao","year":"2009","unstructured":"Zhao, Y., Ciardo, G.: Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 368\u2013381. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_27"},{"issue":"2","key":"4_CR33","first-page":"141","volume":"7","author":"Y Zhao","year":"2011","unstructured":"Zhao, Y., Ciardo, G.: Symbolic computation of strongly connected components and fair cycles using saturation. ISSE 7(2), 141\u2013150 (2011)","journal-title":"ISSE"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"van Dijk, T., van de Pol, J., Meijer, J.: Artifact and instructions to generate experimental results for TACAS 2019 paper: Multi-core On-The-Fly Saturation (artifact). Figshare (2019). https:\/\/doi.org\/10.6084\/m9.figshare.7825406.v1","DOI":"10.6084\/m9.figshare.7825406.v1"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17465-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,15]],"date-time":"2022-09-15T05:34:13Z","timestamp":1663220053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17465-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030174644","9783030174651"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17465-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"164","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"42","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"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"}},{"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"}},{"value":"13","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}