{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:25:12Z","timestamp":1762521912368,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319406473"},{"type":"electronic","value":"9783319406480"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40648-0_20","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"255-271","source":"Crossref","is-referenced-by-count":20,"title":["Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis"],"prefix":"10.1007","author":[{"given":"Jeroen","family":"Meijer","sequence":"first","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"key":"20_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: 13th ACM, VLSI, pp. 116\u2013119. ACM (2003)","DOI":"10.1145\/764808.764839"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-540-85762-4_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"S Blom","year":"2008","unstructured":"Blom, S., van de Pol, J.: Symbolic reachability for process algebras with recursive data types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 81\u201395. Springer, Heidelberg (2008)"},{"issue":"9","key":"20_CR3","doi-asserted-by":"crossref","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":"20_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"20_CR5","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991 (1991)"},{"issue":"1","key":"20_CR6","doi-asserted-by":"crossref","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"},{"issue":"4","key":"20_CR7","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1530873.1530885","volume":"36","author":"G Ciardo","year":"2009","unstructured":"Ciardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the stochastic model checking analyzer for reliability and timing. SIGMETRICS PER 36(4), 58\u201363 (2009)","journal-title":"SIGMETRICS PER"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 359. Springer, Heidelberg (2002)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Cuthill, E., McKee, J.: Reducing the bandwidth of sparse symmetric matrices. In: Proceedings 24th National Conference, pp. 157\u2013172. ACM (1969)","DOI":"10.1145\/800195.805928"},{"issue":"2","key":"20_CR11","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1137\/0713023","volume":"13","author":"NE Gibbs","year":"1976","unstructured":"Gibbs, N.E., Poole Jr., W.G., Stockmeyer, P.K.: An algorithm for reducing the bandwidth and profile of a sparse matrix. SIAM J. Num. Anal. 13(2), 236\u2013250 (1976)","journal-title":"SIAM J. Num. Anal."},{"key":"20_CR12","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1613\/jair.1096","volume":"18","author":"O Grumberg","year":"2003","unstructured":"Grumberg, O., Livne, S., Markovitch, S.: Learning to order BDD variables in verification. JAIR 18, 83\u2013116 (2003)","journal-title":"JAIR"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-38697-8_21","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"M Heiner","year":"2013","unstructured":"Heiner, M., Rohr, C., Schwarick, M.: MARCIE \u2013 model checking and reachability analysis done efficiently. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 389\u2013399. Springer, Heidelberg (2013)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Karantasis, K.I., et al.: Parallelization of reordering algorithms for bandwidth and wavefront reduction. In: ICHPC 2014, pp. 921\u2013932. IEEE (2014)","DOI":"10.1109\/SC.2014.80"},{"key":"20_CR16","volume-title":"Ordering for Optimal Patterns of Structural Matrices","author":"A Kaveh","year":"2006","unstructured":"Kaveh, A.: Ordering for Optimal Patterns of Structural Matrices. Wiley, New York (2006). pp. 191\u2013271"},{"issue":"4","key":"20_CR17","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1002\/nme.1620020406","volume":"2","author":"IP King","year":"1970","unstructured":"King, I.P.: An automatic reordering scheme for simultaneous equations derived from network systems. Int. J. Numer. Meth. Eng. 2(4), 523\u2013533 (1970)","journal-title":"Int. J. Numer. Meth. Eng."},{"key":"20_CR18","unstructured":"Kordon, F., et al.: Complete Results for the 2015 Edition of the Model Checking Contest (2015). http:\/\/mcc.lip6.fr\/2015\/results.php"},{"issue":"2","key":"20_CR19","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008)","journal-title":"STTT"},{"issue":"2","key":"20_CR20","first-page":"183","volume":"52","author":"LO Mafteiu-Scai","year":"2014","unstructured":"Mafteiu-Scai, L.O.: The bandwidths of a matrix. A survey of algorithms. Ann. West Univ. Timisoara-Math. 52(2), 183\u2013223 (2014)","journal-title":"Ann. West Univ. Timisoara-Math."},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"20_CR22","unstructured":"Noack, A.: A ZBDD package for efficient model checking of Petri nets. Forschungsbericht, Branderburgische Technische Uinversit\u00e4t Cottbus (1999)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"issue":"3","key":"20_CR24","doi-asserted-by":"crossref","first-page":"805","DOI":"10.1137\/050629938","volume":"28","author":"JK Reid","year":"2006","unstructured":"Reid, J.K., Scott, J.A.: Reducing the total bandwidth of a sparse unsymmetric matrix. SIAM J. Matrix Anal. Appl. 28(3), 805\u2013821 (2006)","journal-title":"SIAM J. Matrix Anal. Appl."},{"key":"20_CR25","unstructured":"Rice, M., Kulhari, S.: A survey of static variable ordering heuristics for efficient BDD\/MDD construction. Technical report, University of California (2008)"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD1993. IEEE (1993)","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"20_CR27","unstructured":"Rupp, K., Rudolf, F., Weinbub, J.: ViennaCL - a high level linear algebra library for GPUs and multi-core CPUs. In: GPUScA 2010, pp. 51\u201356 (2010)"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/11691372_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RI Siminiceanu","year":"2006","unstructured":"Siminiceanu, R.I., 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)"},{"issue":"11","key":"20_CR29","doi-asserted-by":"crossref","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. Meth. Eng. 28(11), 2651\u20132679 (1989)","journal-title":"Int. J. Numer. Meth. Eng."},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T03:10:58Z","timestamp":1567998658000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}