{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T05:16:08Z","timestamp":1737263768651,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540731955"},{"type":"electronic","value":"9783540731962"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"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":[[2007]]},"DOI":"10.1007\/978-3-540-73196-2_17","type":"book-chapter","created":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T04:50:02Z","timestamp":1183697402000},"page":"263-279","source":"Crossref","is-referenced-by-count":3,"title":["Testing Distributed Systems Through Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Gabriel","family":"Kalyon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Massart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9dric","family":"Meuter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Van Begin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-27860-3_14","volume-title":"Principles of Distributed Systems","author":"B. De Wachter","year":"2004","unstructured":"De Wachter, B., Massart, T., Meuter, C.: dSL: An Environment with Automatic Code Distribution for Industrial Control Systems. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol.\u00a03144, pp. 132\u2013145. Springer, Heidelberg (2004)"},{"issue":"2","key":"17_CR2","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s00165-005-0066-9","volume":"17","author":"B. De Wachter","year":"2005","unstructured":"De Wachter, B., Genon, A., Massart, T., Meuter, C.: The Formal Design of Distributed Controllers with dSL and Spin. Formal Aspects of Computing\u00a017(2), 177\u2013200 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"17_CR3","first-page":"281","volume-title":"FORTE \u201991","author":"T. Massart","year":"1992","unstructured":"Massart, T.: A Calculus to Define Correct Tranformations of LOTOS Specifications. In: FORTE \u201991, pp. 281\u2013296. North-Holland, Amsterdam (1992)"},{"issue":"5","key":"17_CR4","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR5","unstructured":"McMillan, K.: The SMV System. Technical Report CMU-CS-92-131, Carnegie Mellon University (1992)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.M., 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.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032, Springer, Heidelberg (1996)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"17_CR9","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking: an approach to the state explosion problem. Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"issue":"3","key":"17_CR11","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."},{"issue":"7","key":"17_CR12","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"17_CR13","unstructured":"Mattern, F.: Virtual time and global states of distributed systems. In: Proc. Workshop on Parallel and Distributed Algorithms, North-Holland \/ Elsevier, pp. 215\u2013226 (1989)"},{"issue":"4","key":"17_CR14","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s004460050049","volume":"11","author":"C.M. Chase","year":"1998","unstructured":"Chase, C.M., Garg, V.K.: Detection of global predicates: Techniques and their limitations. Distributed Computing\u00a011(4), 191\u2013201 (1998)","journal-title":"Distributed Computing"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Sen, A., Garg, V.K.: Detecting temporal logic predicates in distributed programs using computation slicing. In: OPODIS, pp. 171\u2013183 (2003)","DOI":"10.1007\/978-3-540-27860-3_17"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, pp. 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Mittal, N., Garg, V.K.: Computation slicing: Techniques and theory. In: DISC, pp. 78\u201392 (2001)","DOI":"10.1007\/3-540-45414-4_6"},{"key":"17_CR18","unstructured":"Ganty, P., Meuter, C., Begin, L.V., Kalyon, G., Raskin, J.F., Delzanno, G.: Symbolic data structure for sets of k-uples of integers. Technical Report 570, D\u00e9partement d\u2019Informatique - Universit\u00e9 Libre de Bruxelles (2006)"},{"key":"17_CR19","unstructured":"Ganty, P.: Algorithmes et structures de donn\u00e9es efficaces pour la manipulation de contraintes sur les intervalles. Master\u2019s thesis, Universit\u00e9 Libre de Bruxelles (2002)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.W.: Trace theory. In: Advances in Petri Nets, pp. 279\u2013324 (1986)","DOI":"10.1007\/3-540-17906-2_30"},{"key":"17_CR21","first-page":"438","volume-title":"LICS 1994","author":"P.S. Thiagarajan","year":"1994","unstructured":"Thiagarajan, P.S.: A trace based extension of linear time temporal logic. In: Abramsky, S. (ed.) LICS 1994. Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, pp. 438\u2013447. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Alur, R., Peled, D., Penczek, W.: Model checking of causality properties. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS\u201995), San Diego, California, pp. 90\u2013100 (1995)","DOI":"10.1109\/LICS.1995.523247"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11691372_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Niebert","year":"2006","unstructured":"Niebert, P., Peled, D.: Efficient model checking for ltl with partial order snapshots. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 272\u2013286. Springer, Heidelberg (2006)"},{"issue":"2","key":"17_CR24","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1006\/inco.2001.2956","volume":"179","author":"P.S. Thiagarajan","year":"2002","unstructured":"Thiagarajan, P.S., Walukiewicz, I.: An expressively complete linear time temporal logic for mazurkiewicz traces. Inf. Comput.\u00a0179(2), 230\u2013249 (2002)","journal-title":"Inf. Comput."},{"issue":"2","key":"17_CR25","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1006\/jcss.2001.1817","volume":"64","author":"V. Diekert","year":"2002","unstructured":"Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences\u00a064(2), 396\u2013418 (2002)","journal-title":"Journal of Computer and System Sciences"},{"key":"17_CR26","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M. Nielsen","year":"1981","unstructured":"Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part i. Theor. Comput. Sci.\u00a013, 85\u2013108 (1981)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"17_CR27","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/214451.214456","volume":"3","author":"K.M. Chandy","year":"1985","unstructured":"Chandy, K.M., Lamport, L.: Distributed snapshots: Determining global states of distributed systems. ACM Trans. Comput. Syst.\u00a03(1), 63\u201375 (1985)","journal-title":"ACM Trans. Comput. Syst."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Charron-Bost, B., Delporte-Gallet, C., Fauconnier, H.: Local and temporal predicates in distributed systems. ACM Trans. Program. Lang. Syst. 17(1) (1995)","DOI":"10.1145\/200994.201005"},{"issue":"3","key":"17_CR29","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1109\/71.277788","volume":"5","author":"V.K. Garg","year":"1994","unstructured":"Garg, V.K., Waldecker, B.: Detection of weak unstable predicates in distributed programs. IEEE Trans. Parallel Distrib. Syst.\u00a05(3), 299\u2013307 (1994)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"12","key":"17_CR30","doi-asserted-by":"publisher","first-page":"1323","DOI":"10.1109\/71.553309","volume":"7","author":"V.K. Garg","year":"1996","unstructured":"Garg, V.K., Waldecker, B.: Detection of strong unstable predicates in distributed programs. IEEE Trans. Parallel Distrib. Syst.\u00a07(12), 1323\u20131333 (1996)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Garg, V.K., Mittal, N.: On slicing a distributed computation. In: ICDCS, pp. 322\u2013329 (2001)","DOI":"10.1109\/ICDSC.2001.918962"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Jard, C., J\u00e9ron, T., Jourdan, G.V., Rampon, J.X.: A general approach to trace-checking in distributed computing systems. In: ICDCS, pp. 396\u2013403 (1994)","DOI":"10.1109\/ICDCS.1994.302443"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-540-24730-2_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Sen","year":"2004","unstructured":"Sen, K., Rosu, G., Agha, G.: Online efficient predictive safety analysis of multithreaded programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 123\u2013138. Springer, Heidelberg (2004)"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11494881_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Sen","year":"2005","unstructured":"Sen, K., Rosu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, pp. 211\u2013226. Springer, Heidelberg (2005)"},{"key":"17_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/11813040_37","volume-title":"FM 2006: Formal Methods","author":"A. Genon","year":"2006","unstructured":"Genon, A., Massart, T., Meuter, C.: Monitoring distributed controllers: When an efficient ltl algorithm on sequences is needed to model-check traces. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 557\u2013572. Springer, Heidelberg (2006)"},{"key":"17_CR36","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1109\/DCC.1995.515538","volume-title":"Proceedings of the 5th Data Compression Conference (DCC\u201995)","author":"D. Zampunieris","year":"1995","unstructured":"Zampunieris, D., Le Charlier, B.: Efficient handling of large sets of tuples with sharing trees. In: Proceedings of the 5th Data Compression Conference (DCC\u201995), p. 428. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"17_CR37","unstructured":"Ammirati, P., Delzanno, G., Ganty, P., Geeraerts, G., Raskin, J.F., Van Begin, L.: Babylon: An integrated toolkit for the specification and verification of parameterized systems. In: 2nd workshop on Specification, Analysis and Validation for Emerging technologies (SAVE02) (2002)"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"Kalyon, G., Massart, T., Meuter, C., Van Begin, L.: Testing Distributed System through Symbolic Model Checking. Technical Report 571, D\u00e9partement d\u2019Informatique - Universit\u00e9 Libre de Bruxelles (2007)","DOI":"10.1007\/978-3-540-73196-2_17"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73196-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T06:51:08Z","timestamp":1737183068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73196-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540731955","9783540731962"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73196-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}