{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:29Z","timestamp":1725512009204},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540709510"},{"type":"electronic","value":"9783540709527"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-70952-7_24","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T08:40:01Z","timestamp":1182847201000},"page":"347-361","source":"Crossref","is-referenced-by-count":0,"title":["Distributed Colored Petri Net Model-Checking with Cyclades"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Pajault","sequence":"first","affiliation":[]},{"given":"Jean-Fran\u00e7ois","family":"Pradat-Peyre","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Berthelot, G.: Transformation et analyse de r\u00e9seaux de Petri, applications aux protocoles. Th\u00e8se d\u2019\u00e9tat, Universit\u00e9 Pierre et Marie Curie, Paris (1983)"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Bell, A., Haverkort, B.R.: Sequential and distributed model checking of petri net specifications. Electr. Notes Theor. Comput. Sci.\u00a068(4) (2002)","DOI":"10.1016\/S1571-0661(05)80391-3"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1145\/143165.143235","volume-title":"POPL \u201992: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"E.M. Clarke","year":"1992","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: POPL \u201992: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Albuquerque, New Mexico, United States, pp. 343\u2013354. ACM Press, New York (1992)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A Sweep-Line Method for State Space Exploration. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 450\u2013464. Springer, Heidelberg (2001)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: International Conference on Concurrency Theory, pp. 317\u2013331 (1998), citeseer.nj.nec.com\/cohen98reduction.html","DOI":"10.1007\/BFb0055631"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Haddad, S., Pradat-Peyre, J.F.: New coloured reductions for software validation. In: Work. on Discrete Event Systems, Reims, France (2004)","DOI":"10.1016\/S1474-6670(17)30770-X"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Reliable Software Technology \u2013 Ada-Europe 2005","author":"S. Evangelista","year":"2005","unstructured":"Evangelista, S., Kaiser, C., Pajault, C., Pradat-Peyre, J.F., Rousseau, P.: Dynamic tasks verification with quasar. In: Vardanega, T., Wellings, A.J. (eds.) Ada-Europe 2005. LNCS, vol.\u00a03555, Springer, Heidelberg (2005)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44947-7_12","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2003","author":"S. Evangelista","year":"2003","unstructured":"Evangelista, S., Kaiser, C., Pradat-Peyre, J.F., Rousseau, P.: Quasar: a new tool for analysing concurrent programs. In: Rosen, J.-P., Strohmeier, A. (eds.) Ada-Europe 2003. LNCS, vol.\u00a02655, Springer, Heidelberg (2003)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11767589_9","volume-title":"Petri Nets and Other Models of Concurrency - ICATPN 2006","author":"S. Evangelista","year":"2006","unstructured":"Evangelista, S., Peyre, J.-F.: On the computation of stubborn sets of colored petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol.\u00a04024, Springer, Heidelberg (2006)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/11537328_7","volume-title":"Model Checking Software","author":"S. Evangelista","year":"2005","unstructured":"Evangelista, S., Pradat-Peyre, J.-F.: Memory efficient state space storage in explicit software model checking. In: Godefroid, P. (ed.) Model Checking Software. LNCS, vol.\u00a03639, p. 43. Springer, Heidelberg (2005)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/11494744_26","volume-title":"Applications and Theory of Petri Nets 2005","author":"S. Evangelista","year":"2005","unstructured":"Evangelista, S.: High level petri nets analysis with helena. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol.\u00a03536, pp. 455\u2013464. Springer, Heidelberg (2005)"},{"key":"24_CR12","volume-title":"Electronic Notes in Theoretical Computer Science, vol. 89","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Transactions for software model checking. In: Cook, B., Stoller, S., Visser, W. (eds.) Electronic Notes in Theoretical Computer Science, vol. 89, Elsevier, Amsterdam (2003)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. In: FTfJP 03: Formal Techniques for Java-like Programs (2003)","DOI":"10.5381\/jot.2004.3.6.a4"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 217\u2013234. Springer, Heidelberg (2001)"},{"issue":"2","key":"24_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Form. Methods Syst. Des.\u00a02(2), 149\u2013164 (1993)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Computer Aided Verification","author":"T. Heyman","year":"2000","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 20\u201335. Springer, Heidelberg (2000)"},{"key":"24_CR17","first-page":"339","volume-title":"Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII","author":"G.J. Holzmann","year":"1987","unstructured":"Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, pp. 339\u2013344. North-Holland, Amsterdam (1987)"},{"key":"24_CR18","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proc. of the 3th International SPIN Workshop (1997)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Haddad, S., Pradat-Peyre, J.-F.: New efficient petri nets reductions for parallel programs verification (to appear). Parallel Processing Letters\u00a016(1) (2006)","DOI":"10.1142\/S0129626406002502"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","first-page":"200","volume-title":"Model Checking Software","author":"L. Brim","year":"2001","unstructured":"Brim, L., Barnat, J., Str\u00edbrn\u00e1, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Knottenbelt, W.J., Mestern, M., Harrison, P.G., Kritzinger, P.S.: Probability, parallelism and the state space exploration problem. In: Computer Performance Evaluation (Tools), pp. 165\u2013179 (1998)","DOI":"10.1007\/3-540-68061-6_14"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/978-3-540-27793-4_28","volume-title":"Applications and Theory of Petri Nets 2004","author":"L.M. Kristensen","year":"2004","unstructured":"Kristensen, L.M., Petrucci, L.: An approach to distributed state space exploration for coloured petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol.\u00a03099, pp. 474\u2013483. Springer, Heidelberg (2004)"},{"issue":"12","key":"24_CR23","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"R.J. Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM\u00a018(12), 717\u2013721 (1975), doi:10.1145\/361227.361234","journal-title":"Commun. ACM"},{"key":"24_CR24","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.) Theoretical and Practical Aspects of SPIN Model Checking. LNCS, vol.\u00a01680, pp. 22\u201339. Springer, Heidelberg (1999)"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 80\u2013102. Springer, Heidelberg (2001)"},{"key":"24_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/3-540-44988-4_22","volume-title":"Application and Theory of Petri Nets 2000","author":"D. Poitrenaud","year":"2000","unstructured":"Poitrenaud, D., Pradat-Peyre, J.F.: Pre and post-agglomerations for LTL model checking. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 387\u2013408. Springer, Heidelberg (2000)"},{"key":"24_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11888116_18","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"P. Rousseau","year":"2006","unstructured":"Rousseau, P.: A new approach for concurrent program slicing. In: Najm, E., Pradat-Peyre, J.F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol.\u00a04229, Springer, Heidelberg (2006)"},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 256\u2013278. Springer, Heidelberg (1997)"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Computer Aided Verification","author":"A. Valmari","year":"1993","unstructured":"Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 397\u2013408. Springer, Heidelberg (1993)"},{"key":"24_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-63139-9_40","volume-title":"Application and Theory of Petri Nets 1997","author":"F. Vernadat","year":"1997","unstructured":"Vernadat, F., Michel, F.: Covering step graph preserving failure semantics. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol.\u00a01248, pp. 253\u2013270. Springer, Heidelberg (1997)"},{"issue":"4","key":"24_CR32","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M. Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Transactions on Software Engineering\u00a010(4), 352\u2013357 (1984)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/3-540-56922-7_6","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1993","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 59\u201370. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Applications and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70952-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T14:01:21Z","timestamp":1683900081000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70952-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540709510","9783540709527"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70952-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}