{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:04:59Z","timestamp":1742976299930,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642195822"},{"type":"electronic","value":"9783642195839"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-19583-9_8","type":"book-chapter","created":{"date-parts":[[2011,3,8]],"date-time":"2011-03-08T23:16:56Z","timestamp":1299626216000},"page":"29-45","source":"Crossref","is-referenced-by-count":8,"title":["Debugging Unrealizable Specifications with Model-Based Diagnosis"],"prefix":"10.1007","author":[{"given":"Robert","family":"K\u00f6nighofer","sequence":"first","affiliation":[]},{"given":"Georg","family":"Hofferek","sequence":"additional","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2010","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., K\u00f6nighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY \u2013 A new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 425\u2013429. Springer, Heidelberg (2010)"},{"key":"8_CR2","first-page":"1188","volume-title":"DATE","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: DATE, pp. 1188\u20131193. ACM, New York (2007)"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science\u00a0190(4), 3\u201316 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-44585-4_7","volume-title":"Computer Aided Verification","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Y. Vardi, M.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 66\u201378. Springer, Heidelberg (2001)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-78163-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Cimatti","year":"2008","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 52\u201367. Springer, Heidelberg (2008)"},{"key":"8_CR6","first-page":"139","volume-title":"FMCAD","author":"K. Claessen","year":"2007","unstructured":"Claessen, K.: A coverage analysis for safety property lists. In: FMCAD, pp. 139\u2013145. IEEE, Los Alamitos (2007)"},{"key":"8_CR7","first-page":"1494","volume-title":"IJCAI","author":"L. Console","year":"1993","unstructured":"Console, L., Friedrich, G., Theseider Dupr\u00e9, D.: Model-based diagnosis meets error diagnosis in logic programs. In: IJCAI, pp. 1494\u20131499. Morgan Kaufmann, San Francisco (1993)"},{"key":"8_CR8","first-page":"201","volume-title":"VLSI Design","author":"S. Das","year":"2005","unstructured":"Das, S., Banerjee, A., Basu, P., Dasgupta, P., Chakrabarti, P.P., Mohan, C.R., Fix, L.: Formal methods for analyzing the completeness of an assertion suite against a high-level fault model. In: VLSI Design, pp. 201\u2013206. IEEE, Los Alamitos (2005)"},{"issue":"1","key":"8_CR9","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(87)90063-4","volume":"32","author":"J. Kleer de","year":"1987","unstructured":"de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artificial Intelligence\u00a032(1), 97\u2013130 (1987)","journal-title":"Artificial Intelligence"},{"key":"8_CR10","unstructured":"Dellacherie, S.: Automatic bus-protocol verification using assertions. In: Global Signal Processing Expo Conference, GSPx (2004)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 263\u2013277. Springer, Heidelberg (2009)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"Hardware and Software: Verification and Testing","author":"D. Fisman","year":"2009","unstructured":"Fisman, D., Kupferman, O., Seinvald, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Hoskote, Y.V., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: DAC, pp. 300\u2013305 (1999)","DOI":"10.1145\/309847.309936"},{"key":"8_CR14","first-page":"117","volume-title":"FMCAD","author":"B. Jobstmann","year":"2006","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117\u2013124. IEEE, Los Alamitos (2006)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/3-540-48153-2_21","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Katz","year":"1999","unstructured":"Katz, S., Grumberg, O., Geist, D.: \"Have I written enough properties?\" - A method of comparison between specification and implementation. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 280\u2013297. Springer, Heidelberg (1999)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, R.: Debugging formal specifications with simplified counterstrategies. Master\u2019s thesis, IAIK, Graz University of Technology, Inffeldgasse 16a, A-8010 Graz, Austria (2009)","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"8_CR17","first-page":"152","volume-title":"FMCAD","author":"R. K\u00f6nighofer","year":"2009","unstructured":"K\u00f6nighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: FMCAD, pp. 152\u2013159. IEEE, Los Alamitos (2009)"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"8_CR19","first-page":"531","volume-title":"FOCS","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531\u2013542. IEEE, Los Alamitos (2005)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. CoRR\u00a0abs\/1006.1408 (2010)","DOI":"10.4204\/EPTCS.25.11"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/MDT.2006.5","volume":"23","author":"B. Peischl","year":"2006","unstructured":"Peischl, B., Wotawa, F.: Automated source-level error localization in hardware designs. IEEE Design and Test of Computers\u00a023, 8\u201319 (2006)","journal-title":"IEEE Design and Test of Computers"},{"key":"8_CR22","first-page":"821","volume-title":"DAC","author":"I. Pill","year":"2006","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC, pp. 821\u2013826. ACM, New York (2006)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"8_CR25","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. Artificial Intelligence\u00a032(1), 57\u201395 (1987)","journal-title":"Artificial Intelligence"},{"key":"8_CR26","first-page":"1074","volume-title":"IJCAI","author":"M. Stumptner","year":"1999","unstructured":"Stumptner, M., Wotawa, F.: Debugging functional programs. In: IJCAI, pp. 1074\u20131079. Morgan Kaufmann, San Francisco (1999)"},{"issue":"4","key":"8_CR27","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/S0954-1810(00)00021-2","volume":"14","author":"F. Wotawa","year":"2000","unstructured":"Wotawa, F.: Debugging VHDL designs using model-based reasoning. Artificial Intelligence in Engineering\u00a014(4), 331\u2013351 (2000)","journal-title":"Artificial Intelligence in Engineering"},{"issue":"2","key":"8_CR28","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A. Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering\u00a028(2), 183\u2013200 (2002)","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19583-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T05:54:50Z","timestamp":1558418090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19583-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642195822","9783642195839"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19583-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}