{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:54:47Z","timestamp":1725544487948},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540331025"},{"type":"electronic","value":"9783540331032"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11691617_8","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:14:13Z","timestamp":1143555253000},"page":"126-145","source":"Crossref","is-referenced-by-count":9,"title":["Distributed On-the-Fly Model Checking and Test Case Generation"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Joubert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Mateescu","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. Th. Comp. Sci.\u00a0126(1), 3\u201330 (1994)","journal-title":"Th. Comp. Sci."},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-60045-0_47","volume-title":"Computer Aided Verification","author":"H.R. Andersen","year":"1995","unstructured":"Andersen, H.R., Vergauwen, B.: Efficient Checking of Behavioural Relations and Modal Assertion using Fixed-Point Inversion. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 142\u2013154. Springer, Heidelberg (1995)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-45139-0_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2001","unstructured":"Barnat, J., Brim, L., Stribrna, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-3-540-31980-1_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Bergamini","year":"2005","unstructured":"Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R.: Bisimulator: A Modular Tool for On-the-Fly Equivalence Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 581\u2013585. Springer, Heidelberg (2005)"},{"key":"8_CR5","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 mu-calculus. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 128\u2013147. Springer, Heidelberg (2002)"},{"issue":"2","key":"8_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite- State Concurrent Systems using Temporal Logic Specifications. ACM Trans. on Prog. Lang. and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"issue":"3","key":"8_CR7","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s100090050031","volume":"2","author":"X. Du","year":"1999","unstructured":"Du, X., Smolka, S.A., Cleaveland, R.: Local Model Checking and Protocol Analysis. Int. J. on Software Tools for Technology Transfer (STTT)\u00a02(3), 219\u2013241 (1999)","journal-title":"Int. J. on Software Tools for Technology Transfer (STTT)"},{"key":"8_CR8","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In: Proc. of the 1st LICS, pp. 267\u2013278 (1986)"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional Dynamic Logic of Regular Programs. J. of Computer and System Sciences\u00a018(2), 194\u2013211 (1979)","journal-title":"J. of Computer and System Sciences"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 68\u201384. Springer, Heidelberg (1998)"},{"key":"8_CR11","first-page":"13","volume":"4","author":"H. Garavel","year":"2002","unstructured":"Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. European Assoc. for Software Science and Technology (EASST) Newsletter\u00a04, 13\u201324 (2002)","journal-title":"European Assoc. for Software Science and Technology (EASST) Newsletter"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-36577-X_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Joubert, C.: A Set of Performance and Dependability Analysis Components for Cadp. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 425\u2013430. Springer, Heidelberg (2003)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Holm\u00e9n, F., Leucker, M., Lindstr\u00f6m, M.: UppDMC \u2013 A Distributed Model Checker for Fragments of the \u03bc-calculus. In: Proc. of PDMC 2004. ENTCS, vol.\u00a0128, pp. 91\u2013105 (2004)","DOI":"10.1016\/j.entcs.2004.10.021"},{"key":"8_CR14","volume-title":"The SPIN Model Checker \u2014 Primer and Reference Manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker \u2014 Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"issue":"2","key":"8_CR15","first-page":"187","volume":"7","author":"S.T. Huang","year":"1991","unstructured":"Huang, S.T., Kao, P.W.: Detecting Termination of Distributed Computations by External Agents. J. of Inf. Sci. and Engineering\u00a07(2), 187\u2013201 (1991)","journal-title":"J. of Inf. Sci. and Engineering"},{"issue":"4","key":"8_CR16","first-page":"97","volume":"7","author":"C. Jard","year":"2005","unstructured":"Jard, C., J\u00e9ron, T.: TGV: Theory, Principles and Algorithms. Springer Int. J. on Software Tools for Technology Transfer (STTT)\u00a07(4), 97\u2013315 (2005)","journal-title":"Springer Int. J. on Software Tools for Technology Transfer (STTT)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Joubert, C., Mateescu, R.: Distributed On-the-Fly Equivalence Checking. In: Proc. of PDMC 2004. ENTCS, vol.\u00a0128, pp. 47\u201362 (2004)","DOI":"10.1016\/j.entcs.2004.10.018"},{"key":"8_CR18","volume-title":"Proc. of PDP\u201905","author":"C.. Joubert","year":"2005","unstructured":"Joubert, C., Mateescu, R.: Distributed Local Resolution of Boolean Equation Systems. In: Proc. of PDP 2005. IEEE Computer Society Press, Los Alamitos (2005)"},{"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 \u03bc-calculus. Th. Comp. Sci.\u00a027, 333\u2013354 (1983)","journal-title":"Th. Comp. Sci."},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/BFb0026106","volume-title":"CAAP \u201988","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G.: Proof Systems for Hennessy-Milner logic with Recursion. In: Dauchet, M., Nivat, M. (eds.) CAAP 1988. LNCS, vol.\u00a0299, pp. 215\u2013230. Springer, Heidelberg (1988)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F. Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 22\u201339. Springer, Heidelberg (1999)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Leucker, M., Somla, R., Weber, M.: Parallel Model Checking for LTL, CTL\u2009\u2217\u2009 and L2 \u03bc. In: Proc. of PDMC 2003. ENTCS, vol.\u00a089, pp. 4\u201316 (2003)","DOI":"10.1016\/S1571-0661(05)80093-3"},{"key":"8_CR23","volume-title":"VERSAL","author":"A. Mader","year":"1997","unstructured":"Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. In: VERSAL, vol.\u00a08, Bertz Verlag, Berlin (1997)"},{"key":"8_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems, volume I: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, volume I: Specification. Springer, Heidelberg (1992)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-46419-0_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Mateescu","year":"2000","unstructured":"Mateescu, R.: Efficient Diagnostic Generation for Boolean Equation Systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 251\u2013265. Springer, Heidelberg (2000)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-36577-X_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R.: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 81\u201396. Springer, Heidelberg (2003)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: On-the-fly state space reductions for weak equivalences. In: Proc. of FMICS 2005 (2005)","DOI":"10.1145\/1081180.1081191"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: CAESAR SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems. Int. J. on Software Tools for Technology Transfer (STTT) (2006)","DOI":"10.1007\/s10009-005-0194-9"},{"issue":"3","key":"8_CR29","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Sci. of Comp. Programming\u00a046(3), 255\u2013281 (2003)","journal-title":"Sci. of Comp. Programming"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF01782776","volume":"2","author":"F. Mattern","year":"1987","unstructured":"Mattern, F.: Algorithms for Distributed Termination Detection. Distributed Computing\u00a02, 161\u2013175 (1987)","journal-title":"Distributed Computing"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-45069-6_41","volume-title":"Computer Aided Verification","author":"G. Pace","year":"2003","unstructured":"Pace, G., Lang, F., Mateescu, R.: Calculating \u03c4-Confluence Compositionally. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 446\u2013459. Springer, Heidelberg (2003)"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0054166","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Stevens","year":"1998","unstructured":"Stevens, P., Stirling, C.: Practical Model-Checking using Games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 85\u2013101. Springer, Heidelberg (1998)"},{"issue":"3","key":"8_CR33","first-page":"103","volume":"17","author":"J. Tretmans","year":"1996","unstructured":"Tretmans, J.: Test Generation with Inputs, Outputs and Repetitive Quiescence. Software - Concepts and Tools\u00a017(3), 103\u2013120 (1996)","journal-title":"Software - Concepts and Tools"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,25]],"date-time":"2021-07-25T06:37:56Z","timestamp":1627195076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11691617_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}