{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:08:15Z","timestamp":1743070095212,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319312194"},{"type":"electronic","value":"9783319312200"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-31220-0_6","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:59:52Z","timestamp":1457773192000},"page":"72-85","source":"Crossref","is-referenced-by-count":0,"title":["Fault Localization of Timed Automata Using\u00a0Maximum 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","reference":[{"key":"6_CR1","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":"6_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Proceedings of the EMSOFT 2011, pp. 273\u2013278 (2011)","DOI":"10.1145\/2038642.2038685"},{"key":"6_CR3","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":"6_CR4","unstructured":"Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"key":"6_CR5","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":"6_CR6","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT Solver. \n                      http:\/\/yices.csl.sri.com"},{"issue":"6","key":"6_CR7","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1145\/1993316.1993550","volume":"46","author":"Manu Jose","year":"2011","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses : error localization using maximum satisfiability. In: Proceedings of the PLDI 2011, pp. 437\u2013446 (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"6_CR8","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":"6_CR9","doi-asserted-by":"crossref","unstructured":"Lamraoui, S.-M., Nakajima, S., Hosobe, H.: A hardened flow-sensitive trace formula for fault localization. In: Proceedings of the ICECCS 2015 (2015, to appear)","DOI":"10.1109\/ICECCS.2015.16"},{"issue":"1\u20132","key":"6_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. J. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"J. STTT"},{"key":"6_CR11","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":"6_CR12","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. Autom. Reasoning 40(1), 1\u201333 (2008)","journal-title":"Autom. Reasoning"},{"key":"6_CR13","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":"6_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)"},{"key":"6_CR15","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":"6_CR16","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., Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 378\u2013394. Springer, Heidelberg (2015)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-25141-7_8","volume-title":"Cyber Physical Systems. Design, Modeling, and Evaluation","author":"S Nakajima","year":"2015","unstructured":"Nakajima, S., Lamraoui, S.-M.: Fault localization of energy consumption behavior using maximum satisfiability. In: Mousavi, M.R., Berger, C. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 99\u2013115. Springer, Heidelberg (2015). doi:\n                      10.1007\/978-3-319-25141-7_8"},{"issue":"1","key":"6_CR18","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. Artifi. Intell. 32(1), 57\u201395 (1987)","journal-title":"Artifi. Intell."},{"key":"6_CR19","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":"6_CR20","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"},{"key":"6_CR21","unstructured":"Zhu, C.S., Weissenbacher, G., Malik, S.: Post-silicon fault localization using maximum satisfiability and backbones. In: Proceedings of the FMCAD 2011, pp. 63\u201366 (2011)"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-31220-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:40:20Z","timestamp":1559400020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-31220-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319312194","9783319312200"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-31220-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}