{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T04:23:30Z","timestamp":1743827010363,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642317583"},{"type":"electronic","value":"9783642317590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31759-0_8","type":"book-chapter","created":{"date-parts":[[2012,7,19]],"date-time":"2012-07-19T00:59:50Z","timestamp":1342659590000},"page":"80-97","source":"Crossref","is-referenced-by-count":2,"title":["On Parallel Software Verification Using Boolean Equation Systems"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Ditter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milan","family":"\u010ce\u0161ka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H.R. Andersen","year":"1994","unstructured":"Andersen, H.R.: Model Checking and Boolean Graphs. Theoret. Comp. Sc.\u00a0126(1), 3\u201330 (1994)","journal-title":"Theoret. Comp. Sc."},{"unstructured":"Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley (2000)","key":"8_CR2"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Bauch, P., Brim, L., \u010ce\u0161ka, M.: Computing Strongly Connected Components in Parallel on CUDA. In: IPDPS, pp. 544\u2013555. IEEE (2011)","key":"8_CR3","DOI":"10.1109\/IPDPS.2011.59"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Bauch, P., Brim, L., \u010ce\u0161ka, M.: Designing Fast LTL Model Checking Algorithms for Many-Core GPUs. To app. in J. of Par. and Distrib. Comp. (2012)","key":"8_CR4","DOI":"10.1016\/j.jpdc.2011.10.015"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-73370-6_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable Multi-core LTL Model-Checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 187\u2013203. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Lamr, T.: CUDA Accelerated LTL Model Checking. In: ICPADS, pp. 34\u201341. IEEE (2009)","key":"8_CR6","DOI":"10.1109\/ICPADS.2009.50"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-46017-9_11","volume-title":"Model Checking Software","author":"B. Bollig","year":"2002","unstructured":"Bollig, B., Leucker, M., Weber, M.: Local Parallel Model Checking for the Alternation-Free \u03bc-Calculus. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 128\u2013147. Springer, Heidelberg (2002)"},{"issue":"3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv.\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)","key":"8_CR9"},{"doi-asserted-by":"crossref","unstructured":"Gallardo, M.d.M., Joubert, C., Merino, P.: On-the-Fly Data Flow Analysis Based on Verification Technology. In: COCV. ENTCS, vol.\u00a0190, pp. 33\u201348 (2007)","key":"8_CR10","DOI":"10.1016\/j.entcs.2007.09.006"},{"doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, ch. 16, pp. 995\u20131072. Elsevier (1990)","key":"8_CR11","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1093\/logcom\/exp006","volume":"21","author":"J. Ezekiel","year":"2011","unstructured":"Ezekiel, J., L\u00fcttgen, G., Siminiceanu, R.: To Parallelize or to Optimize? J. of Log. and Comput.\u00a021, 85\u2013120 (2011)","journal-title":"J. of Log. and Comput."},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1839676.1839694","volume":"53","author":"M. Garland","year":"2010","unstructured":"Garland, M., Kirk, D.B.: Understanding Throughput-Oriented Architectures. Commun. ACM\u00a053, 58\u201366 (2010)","journal-title":"Commun. ACM"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10703-005-1493-1","volume":"26","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Heyman, T., Schuster, A.: Distributed Symbolic Model Checking for \u03bc-Calculus. Form. Methods Syst. Des.\u00a026, 197\u2013219 (2005)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-77220-0_21","volume-title":"High Performance Computing \u2013 HiPC 2007","author":"P. Harish","year":"2007","unstructured":"Harish, P., Narayanan, P.J.: Accelerating Large Graph Algorithms on the GPU Using CUDA. In: Aluru, S., Parashar, M., Badrinath, R., Prasanna, V.K. (eds.) HiPC 2007. LNCS, vol.\u00a04873, pp. 197\u2013208. Springer, Heidelberg (2007)"},{"doi-asserted-by":"crossref","unstructured":"Holm\u00e9n, F., Leucker, M., Lindstr\u00f6m, M.: UppDMC: A Distributed Model Checker for Fragments of the mu-Calculus. In: PDMC. ENTCS, vol.\u00a0128, pp. 91\u2013105. Elsevier (2005)","key":"8_CR16","DOI":"10.1016\/j.entcs.2004.10.021"},{"doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bosnacki, D.: Multi-Core Model Checking with SPIN. In: IPDPS, pp. 1\u20138. IEEE (2007)","key":"8_CR17","DOI":"10.1109\/IPDPS.2007.370410"},{"doi-asserted-by":"crossref","unstructured":"Joubert, C., Mateescu, R.: Distributed Local Resolution of Boolean Equation Systems. In: PDP, pp. 264\u2013271. IEEE (2005)","key":"8_CR18","DOI":"10.1109\/EMPDP.2005.19"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the Propositional mu-Calculus. Theoret. Comp. Sc.\u00a027, 333\u2013354 (1983)","journal-title":"Theoret. Comp. Sc."},{"unstructured":"Laarman, A., van de Pol, J., Weber, M.: Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: FMCAD, pp. 247\u2013255. IEEE (2010)","key":"8_CR20"},{"unstructured":"Lefohn, A., Kniss, J.M., Owens, J.D.: Implementing Efficient Parallel Data Structures on GPUs. In: GPU Gems 2, pp. 521\u2013545. Addison-Wesley (2005)","key":"8_CR21"},{"doi-asserted-by":"crossref","unstructured":"Leucker, M., Somla, R., Weber, M.: Parallel Model Checking for LTL, CTL*, and $L^{2}_\\mu$ . In: PDMC. ENTCS, vol.\u00a089, pp. 4\u201316 (2003)","key":"8_CR22","DOI":"10.1016\/S1571-0661(05)80093-3"},{"unstructured":"Mader, A.H.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, Germany (1997)","key":"8_CR23"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10009-005-0194-9","volume":"8","author":"R. Mateescu","year":"2006","unstructured":"Mateescu, R.: CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-free Boolean Equation Systems. STTT\u00a08(1), 37\u201356 (2006)","journal-title":"STTT"},{"doi-asserted-by":"crossref","unstructured":"Merrill, D., Garland, M., Grimshaw, A.: Scalable GPU Graph Traversal. In: PPoPP, pp. 117\u2013128. ACM (2012)","key":"8_CR25","DOI":"10.1145\/2370036.2145832"},{"unstructured":"Nichols, B., Buttlar, D., Farrell, J.P.: PThreads Programming. O\u2019Reilly (1996)","key":"8_CR26"},{"doi-asserted-by":"crossref","unstructured":"van de Pol, J., Weber, M.: A Multi-Core Solver for Parity Games. In: PDMC. ENTCS, vol.\u00a0220, pp. 19\u201334. Elsevier (2008)","key":"8_CR27","DOI":"10.1016\/j.entcs.2008.11.011"},{"unstructured":"Sailer, A.: Utilizing And-Inverter Graphs in the Gaussian Elimination for Boolean Equation Systems. Master\u2019s thesis, Hochschule Regensburg, Germany (2011)","key":"8_CR28"},{"issue":"2","key":"8_CR29","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A.: A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific J. of Math.\u00a05(2), 285\u2013309 (1955)","journal-title":"Pacific J. of Math."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31759-0_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T21:08:41Z","timestamp":1743800921000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31759-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642317583","9783642317590"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31759-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}