{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T01:18:44Z","timestamp":1725671924124},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_38","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"433-448","source":"Crossref","is-referenced-by-count":1,"title":["A Case Study in Verification of Embedded Network Software"],"prefix":"10.1007","author":[{"given":"Kalyan C.","family":"Regula","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hampton","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heather","family":"Harton Keown","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason O.","family":"Hallstrom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nigamanth","family":"Sridhar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"38_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/MIC.2006.37","volume":"10","author":"A. Arora","year":"2006","unstructured":"Arora, A., et al.: Kansei: A high-fidelity sensing testbed. IEEE Intern. Comp.\u00a010(2), 35\u201347 (2006)","journal-title":"IEEE Intern. Comp."},{"issue":"4","key":"38_CR2","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/190679.190683","volume":"19","author":"P. Bucci","year":"1994","unstructured":"Bucci, P., et al.: Part III: Implementing components in resolve. SIGSOFT Softw. Eng. Notes\u00a019(4), 40\u201351 (1994)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"38_CR3","first-page":"7","volume-title":"SEFM 2007","author":"D. Crocker","year":"2007","unstructured":"Crocker, D., Carlton, J.: Verification of c programs using automated reasoning. In: SEFM 2007, pp. 7\u201314. IEEE Computer Society, Washington, DC, USA (2007)"},{"key":"38_CR4","first-page":"1","volume-title":"IC3N 2008","author":"A. Dalton","year":"2008","unstructured":"Dalton, A., et al.: A testbed for visualizing sensornet behavior. In: IC3N 2008, pp. 1\u20137. IEEE Computer Society, Washington DC, USA (2008)"},{"issue":"4","key":"38_CR5","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/190679.190682","volume":"19","author":"S. Edwards","year":"1994","unstructured":"Edwards, S., et al.: Part ii: Specifying components in resolve. SIGSOFT Softw. Eng. Notes\u00a019(4), 29\u201339 (1994)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"38_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"38_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/1352533.1352551","volume-title":"WiSec 2008","author":"Y. Hanna","year":"2008","unstructured":"Hanna, Y., Rajan, H., Zhang, W.: Slede: A domain-specific verification framework for sensor network security protocol implementations. In: WiSec 2008, March 31-April 2, pp. 109\u2013118. ACM, New York (2008)"},{"key":"38_CR8","unstructured":"Harton, H.K.: Modular and Mechanical Verification Condition Generation for Object-Based Software. PhD thesis, Clemson University (2011)"},{"key":"38_CR9","unstructured":"Kulczycki, G.: Direct Reasoning. PhD thesis, Clemson University, Clemson, South Carolina (January 2004)"},{"key":"38_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-27705-4_4","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Kulczycki","year":"2012","unstructured":"Kulczycki, G., Smith, H., Harton, H., Sitaraman, M., Ogden, W.F., Hollingsworth, J.E.: The Location Linking Concept: A Basis for Verification of Code Using Pointers. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 34\u201349. Springer, Heidelberg (2012)"},{"key":"38_CR11","first-page":"2","volume-title":"SEFM 2005","author":"D. Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a c0 compiler: Code generation and implementation correctnes. In: SEFM 2005, pp. 2\u201312. IEEE Computer Society, Washington, DC, USA (2005)"},{"key":"38_CR12","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1145\/958491.958506","volume-title":"SenSys 2003","author":"P. Levis","year":"2003","unstructured":"Levis, P., et al.: Tossim: accurate and scalable simulation of entire tinyos applications. In: SenSys 2003, pp. 126\u2013137. ACM, New York (2003)"},{"key":"38_CR13","doi-asserted-by":"crossref","unstructured":"McCartney, W.P., Sridhar, N.: Abstractions for safe concurrent programming in networked embedded systems. In: SenSys 2006, New York, USA, pp. 167\u2013180 (2006)","DOI":"10.1145\/1182807.1182825"},{"key":"38_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"38_CR15","unstructured":"Schulte, W., et al.: A glimpse of a verifying C compiler. In: C\/C++ Ver. Workshop (July 2007)"},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"Sitaraman, M., et al.: Building a push-button resolve verifier: Progress and challenges. Formal Asp. Comput., 607\u2013626 (2011)","DOI":"10.1007\/s00165-010-0154-3"},{"key":"38_CR17","first-page":"67","volume-title":"IPSN 2005","author":"B. Titzer","year":"2005","unstructured":"Titzer, B., Lee, D., Palsberg, J.: Avrora: scalable sensor network simulation with precise timing. In: IPSN 2005, p. 67. IEEE Press, Piscataway (2005)"},{"issue":"2-4","key":"38_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s10817-009-9120-2","volume":"42","author":"H. Tuch","year":"2009","unstructured":"Tuch, H.: Formal verification of C systems code. J. Autom. Reason.\u00a042(2-4), 125\u2013187 (2009)","journal-title":"J. Autom. Reason."},{"key":"38_CR19","first-page":"68","volume-title":"IPSN 2005","author":"G. Werner-Allen","year":"2005","unstructured":"Werner-Allen, G., Swieskowski, P., Welsh, M.: Motelab: a wireless sensor network testbed. In: IPSN 2005, p. 68. IEEE Press, Piscataway (2005)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:23Z","timestamp":1620126863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}