{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T22:58:56Z","timestamp":1725836336580},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319251400"},{"type":"electronic","value":"9783319251417"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25141-7_8","type":"book-chapter","created":{"date-parts":[[2015,10,31]],"date-time":"2015-10-31T08:51:25Z","timestamp":1446281485000},"page":"99-115","source":"Crossref","is-referenced-by-count":1,"title":["Fault Localization of Energy Consumption Behavior Using Maximum Satisfiability"],"prefix":"10.1007","author":[{"given":"Shin","family":"Nakajima","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Si-Mohamed","family":"Lamraoui","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,1]]},"reference":[{"key":"8_CR1","unstructured":"Android. http:\/\/developer.android.com"},{"key":"8_CR2","unstructured":"IEEE Standard 802.11, Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications (1999)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-56922-7_16","volume-title":"Computer Aided Verification","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A.: Computing accumulated delays in real-time systems. CAV 1993. LNCS, vol. 697, pp. 181\u2013193. Springer, Heidelberg (1993)"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183\u2013235 (1994)","journal-title":"TCS"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci 138, 3\u201324 (1995)","journal-title":"Theoret. Comput. Sci"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"volume-title":"Handbook of Satisfiability","year":"2009","key":"8_CR7","unstructured":"Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Brekling, A., Hansen, M.R., Madsen, J.: MoVES - a framework for modeling and verifying embedded systems. In: Proceedings of the ICM2009, pp. 149\u2013152 (2009)","DOI":"10.1109\/ICM.2009.5418667"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-35873-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Christ","year":"2013","unstructured":"Christ, J., Ermis, E., Sch\u00e4f, M., Wies, T.: Flow-sensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189\u2013208. Springer, Heidelberg (2013)"},{"key":"8_CR10","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT Solver (2006). http:\/\/yices.csl.sri.com"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proceedings of the PLDI 2011, pp. 437\u2013446 (2011)","DOI":"10.1145\/1993316.1993550"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-319-11737-9_17","volume-title":"Formal Methods and Software Engineering","author":"S-M Lamraoui","year":"2014","unstructured":"Lamraoui, S.-M., Nakajima, S.: A formula-based approach for automatic fault localization of imperative programs. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 251\u2013266. Springer, Heidelberg (2014)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11499107_13","volume-title":"Theory and Applications of Satisfiability Testing","author":"MH Liffiton","year":"2005","unstructured":"Liffiton, M.H., Sakallah, K.A.: On finding all minimally unsatisfiable subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 173\u2013186. Springer, Heidelberg (2005)"},{"issue":"1","key":"8_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-38171-3_11","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"MH Liffiton","year":"2013","unstructured":"Liffiton, M.H., Malik, A.: Enumerating infeasibility: finding multiple MUSes quickly. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 160\u2013175. Springer, Heidelberg (2013)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-39611-3_13","volume-title":"Hardware and Software: Verification and Testing","author":"A Morgado","year":"2013","unstructured":"Morgado, A., Liffiton, M., Marques-Silva, J.: MaxSAT-based MCS enumeration. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 86\u2013101. Springer, Heidelberg (2013)"},{"key":"8_CR17","unstructured":"Nakajima, S.: Model-based power consumption analysis of smartphone applications. In: Proceedings of the ACES-MB 2013, pp. 5:1\u20135:10 (2013)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-54624-2_24","volume-title":"Specification, Algebra, and Software","author":"S Nakajima","year":"2014","unstructured":"Nakajima, S.: Everlasting challenges with the OBJ language family. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 478\u2013493. Springer, Heidelberg (2014)"},{"key":"8_CR19","first-page":"3","volume-title":"Proceedings of the 1st CSDM Asia","author":"S Nakajima","year":"2014","unstructured":"Nakajima, S.: Model checking of energy consumption behavior. In: Cardin, M.-A., Krob, D., Lui, P.C., Tan, Y.H., Wood, K. (eds.) Proceedings of the 1st CSDM Asia, pp. 3\u201314. Springer, Switzerland (2014)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-19249-9_24","volume-title":"FM 2015: Formal Methods","author":"S Nakajima","year":"2015","unstructured":"Nakajima, S.: Using real-time maude to model check energy consumption behavior. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 378\u2013394. Springer, Heidelberg (2015)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Nakajima, S.: Formal analysis of android application behavior with real-time maude. In: Proceedings of the CPSNA 2015, pp. 7\u201312 (2015)","DOI":"10.1109\/CPSNA.2015.11"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Pathak, A., Hu, Y.C., Zhang, M.: Bootstrapping energy debugging on smartphones: a first look at energy bugs in mobile devices. In: Proceedings of the Hotnets 2011, pp. 5:1\u20135:6 (2011)","DOI":"10.1145\/2070562.2070567"},{"issue":"1","key":"8_CR23","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Safarpour, S., Mangassarian, H., Veneris, A., Liffiton, M.H., Sakallah, K.A.: Improved design debugging using maximum satisfiability. In: Proceedings of the FMCAD 2007, pp. 13\u201319 (2007)","DOI":"10.1109\/FMCAD.2007.4401977"},{"issue":"5","key":"8_CR25","first-page":"116","volume":"68","author":"M Sorea","year":"2002","unstructured":"Sorea, M.: Bounded model checking for timed automata. ENTCS 68(5), 116\u2013134 (2002)","journal-title":"ENTCS"},{"issue":"4","key":"8_CR26","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1016\/j.jlap.2012.03.002","volume":"81","author":"F Wotawa","year":"2012","unstructured":"Wotawa, F., Nica, M., Moraru, I.: Automated debugging based on a constraint model of the program and a test case. J. Logic Algebraic Program. 81(4), 390\u2013407 (2012)","journal-title":"J. Logic Algebraic Program."}],"container-title":["Lecture Notes in Computer Science","Cyber Physical Systems. Design, Modeling, and Evaluation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25141-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,15]],"date-time":"2023-08-15T18:06:56Z","timestamp":1692122816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25141-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251400","9783319251417"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25141-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}