{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:39:53Z","timestamp":1725791993827},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319069319"},{"type":"electronic","value":"9783319069326"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06932-6_31","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T11:14:18Z","timestamp":1397819658000},"page":"323-334","source":"Crossref","is-referenced-by-count":1,"title":["An Effective Way of Storing and Accessing Very Large Transition Matrices Using Multi-core CPU and GPU Architectures"],"prefix":"10.1007","author":[{"given":"Bo\u017cena","family":"Wieczorek","sequence":"first","affiliation":[]},{"given":"Marcin","family":"Po\u0142omski","sequence":"additional","affiliation":[]},{"given":"Piotr","family":"Pecka","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Deorowicz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"Baskaran, M., Bordawekar, R.: Optimizing sparse matrix-vector multiplication on GPUs using compile-time and run-time strategies. Tech. Rep. RC24704 (W0812-047), IBM Research Report (2008)"},{"key":"31_CR2","unstructured":"Bell, N., Garland, M.: Efficient sparse matrix-vector multiplication on cuda. Tech. Rep. NVR-2008-004, NVIDIA Technical Report (2008)"},{"key":"31_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"B. Berard","year":"2001","unstructured":"Berard, B., Bidoit, M., Finkel, A.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Berlin (2001)"},{"key":"31_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"31_CR5","doi-asserted-by":"publisher","first-page":"1077","DOI":"10.1002\/spe.402","volume":"31","author":"M. Ciura","year":"2001","unstructured":"Ciura, M., Deorowicz, S.: How to squeeze a lexicon. Software\u2013Practice and Experience\u00a031, 1077\u20131090 (2001)","journal-title":"Software\u2013Practice and Experience"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/BFb0022197","volume-title":"Computer Performance Evaluation Modelling Techniques and Tools","author":"D. Deavours","year":"1997","unstructured":"Deavours, D., Sanders, W.: An efficient disk-based tool for solving very large markov models. In: Marie, R., Plateau, B., Calzarossa, M.C., Rubino, G.J. (eds.) TOOLS 1997. LNCS, vol.\u00a01245, pp. 58\u201371. Springer, Heidelberg (1997)"},{"key":"31_CR7","unstructured":"Edmund, M., Clarke, J., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Kikuchi, S., Matsumoto, Y.: Performance modeling of concurrent live migration operations in cloud computing systems using PRISM probabilistic model checker. In: Proceedings of the 4th International Conference on Cloud Computing, pp. 49\u201356 (2011)","DOI":"10.1109\/CLOUD.2011.48"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-39640-3_15","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2013","author":"D. Mukunoki","year":"2013","unstructured":"Mukunoki, D., Takahashi, D.: Optimization of sparse matrix-vector multiplication for CRS format on NVIDIA kepler architecture GPUs. In: Murgante, B., Misra, S., Carlini, M., Torre, C.M., Nguyen, H.-Q., Taniar, D., Apduhan, B.O., Gervasi, O. (eds.) ICCSA 2013, Part V. LNCS, vol.\u00a07975, pp. 211\u2013223. Springer, Heidelberg (2013)"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-14891-0_21","volume-title":"Smart Spaces and Next Generation Wired\/Wireless Networking","author":"M. Nowak","year":"2010","unstructured":"Nowak, M., Pecka, P.: Reducing the number of states for markovian model of optical slotted ring network. In: Balandin, S., Dunaytsev, R., Koucheryavy, Y. (eds.) ruSMART 2010. LNCS, vol.\u00a06294, pp. 231\u2013241. Springer, Heidelberg (2010)"},{"key":"31_CR12","unstructured":"OpenMP 2002: OpenMP architecture review board, OpenMP C and C++ application program interface (2002), \n http:\/\/www.openmp.org\/mp-documents\/cspec20.pdf"},{"key":"31_CR13","unstructured":"Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham (2002)"},{"key":"31_CR14","series-title":"AISC","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-23169-8_49","volume-title":"Man-Machine Interactions 2","author":"P. Pecka","year":"2011","unstructured":"Pecka, P., Deorowicz, S., Nowak, M.: Efficient Representation of Transition Matrix in the Markov Process Modeling of Computer Networks. In: Czach\u00f3rski, T., Kozielski, S., Sta\u0144czyk, U. (eds.) Man-Machine Interactions 2. AISC, vol.\u00a0103, pp. 457\u2013464. Springer, Heidelberg (2011)"},{"key":"31_CR15","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1504\/IJCCBS.2011.042331","volume":"2","author":"D. Rabih","year":"2011","unstructured":"Rabih, D., Gorgo, G., Pekergin, N., Vincent, J.: Steady state property verification of very large systems. International Journal of Critical Computer-Based Systems\u00a02, 309\u2013331 (2011)","journal-title":"International Journal of Critical Computer-Based Systems"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D. El Rabih","year":"2009","unstructured":"El Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 120\u2013134. Springer, Heidelberg (2009)"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","first-page":"121","volume-title":"Information Management in Computer Integrated Manufacturing","author":"Y. Saad","year":"1995","unstructured":"Saad, Y.: Projection methods for solving large sparse eigenvalue problems. In: Adelsberger, H.H., Lazansk\u00fd, J., Ma\u0159\u00edk, V. (eds.) Education in CIM 1995. LNCS, vol.\u00a0973, pp. 121\u2013144. Springer, Heidelberg (1995)"},{"key":"31_CR18","unstructured":"Sidje, R.: Parallel Algorithms for Large Sparse Matrix Exponentials: application to numerical transient analysis of Markov processes. Ph.D. thesis, University of Rennes (1994)"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Stewart, W.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)","DOI":"10.1515\/9780691223384"},{"key":"31_CR20","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2001","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal\u00a010, 203\u2013232 (2001)","journal-title":"Automated Software Engineering Journal"}],"container-title":["Communications in Computer and Information Science","Beyond Databases, Architectures, and Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06932-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T00:43:55Z","timestamp":1676853835000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-06932-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319069319","9783319069326"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06932-6_31","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2014]]}}}