{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:11:25Z","timestamp":1772039485523,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,11,16]],"date-time":"2016-11-16T00:00:00Z","timestamp":1479254400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,11,16]]},"DOI":"10.1145\/2993422.2993426","type":"proceedings-article","created":{"date-parts":[[2016,11,2]],"date-time":"2016-11-02T12:22:17Z","timestamp":1478089337000},"page":"133-142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":47,"title":["Systematically Debugging IoT Control System Correctness for Building Automation"],"prefix":"10.1145","author":[{"given":"Chieh-Jan Mike","family":"Liang","sequence":"first","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Bu","sequence":"additional","affiliation":[{"name":"Nanjing University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhao","family":"Li","sequence":"additional","affiliation":[{"name":"Microsoft Research and University of Science and Technology of China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junbei","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microsoft Research and University of Science and Technology of China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shi","family":"Han","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B\u00f6rje F.","family":"Karlsson","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dongmei","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feng","family":"Zhao","sequence":"additional","affiliation":[{"name":"Microsoft Research"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,11,16]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"AllJoyn. http:\/\/www.alljoyn.org.  AllJoyn. http:\/\/www.alljoyn.org."},{"key":"e_1_3_2_2_2_1","unstructured":"IFTTT\n  : Put the internet to work for you. http:\/\/ifttt.com.  IFTTT: Put the internet to work for you. http:\/\/ifttt.com."},{"key":"e_1_3_2_2_3_1","unstructured":"Thread. http:\/\/threadgroup.org.  Thread. http:\/\/threadgroup.org."},{"key":"e_1_3_2_2_4_1","unstructured":"WSU CASAS Datasets. http:\/\/ailab.wsu.edu\/casas\/datasets.  WSU CASAS Datasets. http:\/\/ailab.wsu.edu\/casas\/datasets."},{"key":"e_1_3_2_2_5_1","unstructured":"Amazon. Device Registry for AWS IoT. http:\/\/docs.aws.amazon.com\/iot\/latest\/developerguide\/thing-registry.html.  Amazon. Device Registry for AWS IoT. http:\/\/docs.aws.amazon.com\/iot\/latest\/developerguide\/thing-registry.html."},{"key":"e_1_3_2_2_6_1","unstructured":"Apple. HomeKit. http:\/\/developer.apple.com\/homekit.  Apple. HomeKit. http:\/\/developer.apple.com\/homekit."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604140"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0132-2"},{"key":"e_1_3_2_2_9_1","unstructured":"Belkin. Wemo. http:\/\/www.belkin.com\/us\/Products\/c\/home-automation.  Belkin. Wemo. http:\/\/www.belkin.com\/us\/Products\/c\/home-automation."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1978942.1979249"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000367.2000368"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985811"},{"key":"e_1_3_2_2_13_1","volume-title":"A framework for counterexample generation and exploration. STTT, 9(5-6)","author":"Chechik M.","year":"2007","unstructured":"M. Chechik and A. Gurfinkel . A framework for counterexample generation and exploration. STTT, 9(5-6) , 2007 . M. Chechik and A. Gurfinkel. A framework for counterexample generation and exploration. STTT, 9(5-6), 2007."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2029932.2029934"},{"key":"e_1_3_2_2_15_1","volume-title":"NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking","author":"Cimatti A.","year":"2002","unstructured":"A. Cimatti , E. Clarke , E. Giunchiglia , F. Giunchiglia , M. Pistore , M. Roveri , R. Sebastiani , and A. Tacchella . NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking . In CAV. Springer , 2002 . A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In CAV. Springer, 2002."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_2_17_1","volume-title":"http:\/\/cnn.com\/2013\/08\/14\/opinion\/schneier-hacking-baby-monitor\/","author":"Why It's So CNN.","year":"2013","unstructured":"CNN. Why It's So Easy To Hack Your Home . http:\/\/cnn.com\/2013\/08\/14\/opinion\/schneier-hacking-baby-monitor\/ , 2013 . CNN. Why It's So Easy To Hack Your Home. http:\/\/cnn.com\/2013\/08\/14\/opinion\/schneier-hacking-baby-monitor\/, 2013."},{"key":"e_1_3_2_2_18_1","volume-title":"ATC. USENIX","author":"Croft J.","year":"2015","unstructured":"J. Croft , R. Mahajan , M. Caesar , and M. Musuvathi . Systematically Exploring the Behavior of Control Programs . In ATC. USENIX , 2015 . J. Croft, R. Mahajan, M. Caesar, and M. Musuvathi. Systematically Exploring the Behavior of Control Programs. In ATC. USENIX, 2015."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_5"},{"key":"e_1_3_2_2_21_1","volume-title":"NSDI. USENIX","author":"Dixon C.","year":"2012","unstructured":"C. Dixon , R. Mahajan , S. Agarwal , A. B. Brush , B. Lee , S. Saroiu , and P. Bahl . An Operating System for the Home . In NSDI. USENIX , 2012 . C. Dixon, R. Mahajan, S. Agarwal, A. B. Brush, B. Lee, S. Saroiu, and P. Bahl. An Operating System for the Home. In NSDI. USENIX, 2012."},{"key":"e_1_3_2_2_22_1","unstructured":"Google. Weave. http:\/\/developers.google.com\/weave.  Google. Weave. http:\/\/developers.google.com\/weave."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.032"},{"key":"e_1_3_2_2_24_1","volume-title":"TACAS","author":"Groce A.","year":"2004","unstructured":"A. Groce . Error Explanation with Distance Metrics . In TACAS , 2004 . A. Groce. Error Explanation with Distance Metrics. In TACAS, 2004."},{"key":"e_1_3_2_2_25_1","volume-title":"LICS","author":"Henzinger T. A.","year":"1996","unstructured":"T. A. Henzinger . The Theory of Hybrid Automata . In LICS , 1996 . T. A. Henzinger. The Theory of Hybrid Automata. In LICS, 1996."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.760724"},{"key":"e_1_3_2_2_27_1","volume-title":"State of the Smart Home","year":"2015","unstructured":"Icontrol. State of the Smart Home 2015 . Technical report, 2015. Icontrol. State of the Smart Home 2015. Technical report, 2015."},{"key":"e_1_3_2_2_28_1","unstructured":"Insteon. Insteon. http:\/\/insteon.com.  Insteon. Insteon. http:\/\/insteon.com."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.05.005"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993550"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737095.2737115"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384626"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/EWSN.2005.1462020"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1674-7_38"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2014.6843717"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79576-6_13"},{"key":"e_1_3_2_2_37_1","unstructured":"P. Nolan and M. Adair. Untangling The Web Of Liability In The Internet Of Things. http:\/\/www.mhc.ie\/latest\/untangling-the-web-of-liability-in-the-internet-of-things.  P. Nolan and M. Adair. Untangling The Web Of Liability In The Internet Of Things. http:\/\/www.mhc.ie\/latest\/untangling-the-web-of-liability-in-the-internet-of-things."},{"key":"e_1_3_2_2_38_1","unstructured":"Nominet. Nominet IoT Registry. http:\/\/nominet.uk.  Nominet. Nominet IoT Registry. http:\/\/nominet.uk."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1006\/ijhc.2000.0410"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001445"},{"key":"e_1_3_2_2_41_1","volume-title":"Dagstuhl Reports","author":"Pezz\u00e8 M.","year":"2011","unstructured":"M. Pezz\u00e8 , M. C. Rinard , W. Weimer , and A. Zeller . Self-repairing Programs . In Dagstuhl Reports , 2011 . M. Pezz\u00e8, M. C. Rinard, W. Weimer, and A. Zeller. Self-repairing Programs. In Dagstuhl Reports, 2011."},{"key":"e_1_3_2_2_42_1","unstructured":"Philips. Hue. http:\/\/www.meethue.com.  Philips. Hue. http:\/\/www.meethue.com."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517451"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081749"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2556288.2557420"},{"key":"e_1_3_2_2_46_1","volume-title":"State of the Market - The Internet of Things","year":"2015","unstructured":"Verizon. State of the Market - The Internet of Things 2015 . Technical report, 2015. Verizon. State of the Market - The Internet of Things 2015. Technical report, 2015."},{"key":"e_1_3_2_2_47_1","unstructured":"W3C. Schema.org. http:\/\/schema.org.  W3C. Schema.org. http:\/\/schema.org."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831716"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182807.1182822"}],"event":{"name":"BuildSys '16: The 3rd ACM International Conference on Systems for Energy-Efficient Built Environments","location":"Palo Alto CA USA","acronym":"BuildSys '16","sponsor":["SIGMETRICS ACM Special Interest Group on Measurement and Evaluation","SIGCOMM ACM Special Interest Group on Data Communication","SIGMOBILE ACM Special Interest Group on Mobility of Systems, Users, Data and Computing","SIGOPS ACM Special Interest Group on Operating Systems","SIGBED ACM Special Interest Group on Embedded Systems","SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 3rd ACM International Conference on Systems for Energy-Efficient Built Environments"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2993422.2993426","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2993422.2993426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:23Z","timestamp":1750218623000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2993422.2993426"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,16]]},"references-count":49,"alternative-id":["10.1145\/2993422.2993426","10.1145\/2993422"],"URL":"https:\/\/doi.org\/10.1145\/2993422.2993426","relation":{},"subject":[],"published":{"date-parts":[[2016,11,16]]},"assertion":[{"value":"2016-11-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}