{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:18:28Z","timestamp":1745986708020,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642358722"},{"type":"electronic","value":"9783642358739"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35873-9_30","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T06:22:57Z","timestamp":1357107777000},"page":"515-535","source":"Crossref","is-referenced-by-count":4,"title":["State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction"],"prefix":"10.1007","author":[{"given":"Manchun","family":"Zheng","sequence":"first","affiliation":[]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Yu","family":"Gu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"Experiment Materials, http:\/\/www.comp.nus.edu.sg\/~pat\/NesC\/por"},{"issue":"4","key":"30_CR2","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S1389-1286(01)00302-4","volume":"38","author":"I. Akyildiz","year":"2002","unstructured":"Akyildiz, I., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless Sensor Networks: a Survey. Computer Networks\u00a038(4), 393\u2013422 (2002)","journal-title":"Computer Networks"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Archer, W., Levis, P., Regehr, J.: Interface contracts for TinyOS. In: IPSN, Massachusetts, USA, pp. 158\u2013165 (2007)","DOI":"10.1145\/1236360.1236382"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-05408-2_12","volume-title":"Ambient Intelligence","author":"D. Bucur","year":"2009","unstructured":"Bucur, D., Kwiatkowska, M.: Bug-Free Sensors: The Automatic Verification of Context-Aware TinyOS Applications. In: Tscheligi, M., de Ruyter, B., Markopoulus, P., Wichert, R., Mirlacher, T., Meschterjakov, A., Reitberger, W. (eds.) AmI 2009. LNCS, vol.\u00a05859, pp. 101\u2013105. Springer, Heidelberg (2009)"},{"issue":"10","key":"30_CR5","doi-asserted-by":"publisher","first-page":"1693","DOI":"10.1016\/j.jss.2011.04.054","volume":"84","author":"D. Bucur","year":"2011","unstructured":"Bucur, D., Kwiatkowska, M.Z.: On software verification for sensor nodes. Journal of Systems and Software\u00a084(10), 1693\u20131707 (2011)","journal-title":"Journal of Systems and Software"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-45449-7_9","volume-title":"Embedded Software","author":"D.E. Culler","year":"2001","unstructured":"Culler, D.E., Hill, J., Buonadonna, P., Szewczyk, R., Woo, A.: A Network-Centric Approach to Embedded Software for Tiny Devices. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 114\u2013130. Springer, Heidelberg (2001)"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Dunkels, A., Gr\u00f6nvall, B., Voigt, T.: Contiki - A Lightweight and Flexible Operating System for Tiny Networked Sensors. In: LCN, pp. 455\u2013462 (2004)","DOI":"10.1109\/LCN.2004.38"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110\u2013121. ACM (2005)","DOI":"10.1145\/1047659.1040315"},{"issue":"5","key":"30_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/780822.781133","volume":"38","author":"David Gay","year":"2003","unstructured":"Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., Culler, D.: The nesC Language: A Holistic Approach to Networked Embedded Systems. In: PLDI, pp. 1\u201311 (2003)","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"30_CR11","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. Formal Methods in System Design\u00a02(2), 149\u2013164 (1993)","journal-title":"Formal Methods in System Design"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"Model Checking Software","author":"G. Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian Partial-Order Reduction. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 95\u2013112. Springer, Heidelberg (2007)"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Hanna, Y., Rajan, H., Zhang, W.: SLEDE: a domain-specific verification framework for sensor network security protocol implementations. In: WISEC, pp. 109\u2013118 (2008)","DOI":"10.1145\/1352533.1352551"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Levis, P., Gay, D.: TinyOS Programming, 1st edn. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511626609"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Levis, P., Lee, N., Welsh, M., Culler, D.E.: TOSSIM: Accurate and Scalable Simulation of Entire TinyOS Applications. In: SenSys, pp. 126\u2013137 (2003)","DOI":"10.1145\/958503.958506"},{"key":"30_CR16","unstructured":"Levis, P., Patel, N., Culler, D.E., Shenker, S.: Trickle: A Self-Regulating Algorithm for Code Propagation and Maintenance in Wireless Sensor Networks. In: NSDI, California, USA, pp. 15\u201328 (2004)"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Li, P., Regehr, J.: T-Check: bug finding for sensor networks. In: IPSN, Stockholm, Sweden, pp. 174\u2013185 (2010)","DOI":"10.1145\/1791212.1791234"},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/11537328_16","volume-title":"Model Checking Software","author":"B. Luttik","year":"2005","unstructured":"Luttik, B., Tr\u010dka, N.: Stuttering Congruence for Chi. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 185\u2013199. Springer, Heidelberg (2005)"},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"McInnes, A.I.: Using CSP to Model and Analyze TinyOS Applications. In: ECBS, California, USA, pp. 79\u201388 (2009)","DOI":"10.1109\/ECBS.2009.34"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Mottola, L., Voigt, T., Osterlind, F., Eriksson, J., Baresi, L., Ghezzi, C.: Anquiro: Enabling Efficient Static Verification of Sensor Network Software. In: SESENA, pp. 32\u201337 (2010)","DOI":"10.1145\/1809111.1809122"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: ESEC\/SIGSOFT FSE, pp. 267\u2013276 (2003)","DOI":"10.1145\/949952.940107"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: A Flexible Framework for Creating Software Model Checkers. In: TAIC PART, pp. 3\u201322 (2006)","DOI":"10.1109\/TAIC-PART.2006.5"},{"key":"30_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-15898-8_8","volume-title":"Formal Methods for Industrial Critical Systems","author":"F. Werner","year":"2010","unstructured":"Werner, F., Farag\u00f3, D.: Correctness of Sensor Network Applications by Software Bounded Model Checking. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol.\u00a06371, pp. 115\u2013131. Springer, Heidelberg (2010)"},{"key":"30_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-85114-1_20","volume-title":"Model Checking Software","author":"Y. Yang","year":"2008","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.C., Kirby, R.M.: Efficient Stateful Dynamic Partial Order Reduction. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 288\u2013305. Springer, Heidelberg (2008)"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-24559-6_26","volume-title":"Formal Methods and Software Engineering","author":"M. Zheng","year":"2011","unstructured":"Zheng, M., Sun, J., Liu, Y., Dong, J.S., Gu, Y.: Towards a Model Checker for NesC and Wireless Sensor Networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 372\u2013387. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35873-9_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T15:33:38Z","timestamp":1745940818000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35873-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642358722","9783642358739"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35873-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}