{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T13:24:37Z","timestamp":1726061077222},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642116223"},{"type":"electronic","value":"9783642116230"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11623-0_7","type":"book-chapter","created":{"date-parts":[[2010,1,24]],"date-time":"2010-01-24T20:08:29Z","timestamp":1264363709000},"page":"129-145","source":"Crossref","is-referenced-by-count":13,"title":["Towards a Notion of Unsatisfiable Cores for LTL"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Prosyd, http:\/\/www.prosyd.org\/"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"R. Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection in linear temporal logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 368\u2013380. Springer, Heidelberg (2003)"},{"key":"7_CR3","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR4","unstructured":"Bakker, R., Dikker, F., Tempelman, F.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI (1993)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Formal Methods in System Design\u00a018(2) (2001)","DOI":"10.1023\/A:1008779610539"},{"key":"7_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.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science\u00a02(5) (2006)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73368-3_30","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Cavada, R., Pill, I., Roveri, M., Tchaltsev, A.: RAT: A tool for the formal analysis of requirements. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Bruni, R., Sassano, A.: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. In: SAT (2001)","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Chinneck, J., Dravnieks, E.: Locating minimal infeasible constraint sets in linear programs. ORSA Journal on Computing\u00a03(2) (1991)","DOI":"10.1287\/ijoc.3.2.157"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Beyond vacuity: Towards the strongest passing formula. In: FMCAD (2008)","DOI":"10.1109\/FMCAD.2008.ECP.28"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Chockler, H., Kupferman, O., Vardi, M.: Coverage metrics for temporal logic model checking. Formal Methods in System Design\u00a028(3) (2006)","DOI":"10.1007\/s10703-006-0001-6"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Chockler, H., Strichman, O.: Easier and more informative vacuity checks. In: MEMOCODE (2007)","DOI":"10.1109\/MEMCOD.2007.371225"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-72788-0_32","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 334\u2013339. Springer, Heidelberg (2007)"},{"key":"7_CR15","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":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-540-73368-3_53","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2007","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 532\u2013546. Springer, Heidelberg (2007)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/978-3-540-30494-4_18","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 245\u2013259. Springer, Heidelberg (2004)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-642-03240-0_15","volume-title":"FMICS 2008","author":"A. Cimatti","year":"2009","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: From informal requirements to property-driven formal validation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol.\u00a05596, pp. 166\u2013181. Springer, Heidelberg (2009)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Formal Methods in System Design\u00a010(1) (1997)","DOI":"10.1023\/A:1008615614281"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-540-24605-3_7","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 78\u201392. Springer, Heidelberg (2004)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814948_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 36\u201341. Springer, Heidelberg (2006)"},{"key":"7_CR22","unstructured":"Fisher, M.: A resolution method for temporal logic. In: IJCAI (1991)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log.\u00a02(1) (2001)","DOI":"10.1145\/371282.371311"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"HVC 2008","author":"D. Fisman","year":"2009","unstructured":"Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/978-3-540-74970-7_24","volume-title":"CP 2007","author":"\u00c9. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: MUST: Provide a finer-grained explanation of unsatisfiability. In: Bessiere, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 317\u2013331. Springer, Heidelberg (2007)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/978-3-540-24730-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous? In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 451\u2013466. Springer, Heidelberg (2004)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/11513988_10","volume-title":"Computer Aided Verification","author":"K. Heljanko","year":"2005","unstructured":"Heljanko, K., Junttila, T., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 98\u2013111. Springer, Heidelberg (2005)"},{"key":"7_CR30","volume-title":"Decision Procedures","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT\u00a04(2) (2003)","DOI":"10.1007\/s100090100062"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"K. Namjoshi","year":"2001","unstructured":"Namjoshi, K.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 2. Springer, Heidelberg (2001)"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-540-27813-9_5","volume-title":"Computer Aided Verification","author":"K. Namjoshi","year":"2004","unstructured":"Namjoshi, K.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 57\u201369. Springer, Heidelberg (2004)"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"D. Peled","year":"2001","unstructured":"Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, p. 292. Springer, Heidelberg (2001)"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC (2006)","DOI":"10.1145\/1146909.1147119"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02(3) (1986)","DOI":"10.1016\/S0747-7171(86)80028-1"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. POPL (1989)","DOI":"10.1145\/75277.75293"},{"key":"7_CR39","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-75560-9_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Samer","year":"2007","unstructured":"Samer, M., Veith, H.: On the notion of vacuous truth. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 2\u201314. Springer, Heidelberg (2007)"},{"key":"7_CR40","volume-title":"IJCAI","author":"S. Schlobach","year":"2003","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: IJCAI. Morgan Kaufmann, San Francisco (2003)"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Towards a notion of unsatisfiable cores for LTL. Technical Report 200901000, Fondazione Bruno Kessler (2009)","DOI":"10.1007\/978-3-642-11623-0_7"},{"key":"7_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: ASE (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: FMCAD (2007)","DOI":"10.1109\/FAMCAD.2007.16"},{"key":"7_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-68237-0_23","volume-title":"FM 2008: Formal Methods","author":"E. Torlak","year":"2008","unstructured":"Torlak, E., Chang, F., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 326\u2013341. Springer, Heidelberg (2008)"},{"key":"7_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1007\/11574620_53","volume-title":"The Semantic Web \u2013 ISWC 2005","author":"H. Wang","year":"2005","unstructured":"Wang, H., Horridge, M., Rector, A., Drummond, N., Seidenberg, J.: Debugging OWL-DL ontologies: A heuristic approach. In: Gil, Y., Motta, E., Benjamins, V.R., Musen, M.A. (eds.) ISWC 2005. LNCS, vol.\u00a03729, pp. 745\u2013757. Springer, Heidelberg (2005)"},{"key":"7_CR47","volume-title":"IJCAI","author":"S. Wolfman","year":"1999","unstructured":"Wolfman, S., Weld, D.: The LPSAT engine & its application to resource planning. In: IJCAI. Morgan Kaufmann, San Francisco (1999)"},{"key":"7_CR48","unstructured":"Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable Boolean formula. Presented at SAT (2003)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11623-0_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:42:26Z","timestamp":1606167746000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11623-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642116223","9783642116230"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11623-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}