{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:03:00Z","timestamp":1777125780348,"version":"3.51.4"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T00:00:00Z","timestamp":1262736000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1007\/s10009-009-0134-1","type":"journal-article","created":{"date-parts":[[2010,1,5]],"date-time":"2010-01-05T13:27:30Z","timestamp":1262698050000},"page":"319-335","source":"Crossref","is-referenced-by-count":11,"title":["Exploiting resolution proofs to speed up LTL vacuity detection for BMC"],"prefix":"10.1007","volume":"12","author":[{"given":"Jocelyn","family":"Simmonds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jessica","family":"Davies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,1,6]]},"reference":[{"key":"134_CR1","doi-asserted-by":"crossref","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection in linear temporal logic. In: Proceedings of the 15th International Conference on Computer Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 368\u2013380 (2003)","DOI":"10.1007\/978-3-540-45069-6_35"},{"key":"134_CR2","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Proceedings of the 9th International Conference on Computer Aided Verification (CAV\u201997). Lecture Notes in Computer Science, vol. 1254, pp. 279\u2013290 (1997)","DOI":"10.1007\/3-540-63166-6_28"},{"issue":"2","key":"134_CR3","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I. Beer","year":"2001","unstructured":"Beer I., Ben-David S., Eisner C., Rodeh Y.: Efficient detection of vacuity in temporal model checking. Formal Methods Syst. Des. (FMSD) 18(2), 141\u2013163 (2001)","journal-title":"Formal Methods Syst. Des. (FMSD)"},{"key":"134_CR4","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999). Lecture Notes in Computer Science, vol. 1579 (1999)","DOI":"10.21236\/ADA360973"},{"key":"134_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV\u201902). Lecture Notes in Computer Science, vol. 2404, pp. 359\u2013364 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"134_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Sebastiani, R.: Improving the encoding of LTL model checking into SAT. In: Proceedings of the 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201902). Lecture Notes in Computer Science, vol. 2294, pp. 196\u2013207 (2002)","DOI":"10.1007\/3-540-47813-2_14"},{"key":"134_CR7","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke E., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"3","key":"134_CR8","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig W.: Linear reasoning. A new form of the Herbrand\u2013Gentzen theorem. J. Symb. Logic (JSL) 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Logic (JSL)"},{"key":"134_CR9","doi-asserted-by":"crossref","unstructured":"Dong, Y., Sarna-Starosta, B., Ramakrishnan, C.R., Smolka, S.A.: Vacuity checking in the modal Mu-Calculus. In: Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology (AMAST\u201902). Lecture Notes in Computer Science, vol. 2422, pp. 147\u2013162. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45719-4_11"},{"key":"134_CR10","unstructured":"Een, N., S\u00f6rensson, N.: The MiniSat Page. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/Main.html . April (2006)"},{"key":"134_CR11","doi-asserted-by":"crossref","unstructured":"Gershman, R., Koifman, M., Strichman, O.: Deriving small unsatisfiable cores with dominators. In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201906). Lecture Notes in Computer Science, vol. 4144, pp. 109\u2013122 (2006)","DOI":"10.1007\/11817963_13"},{"key":"134_CR12","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201904). Lecture Notes in Computer Science, vol. 3312, pp. 306\u2013321 (2004)","DOI":"10.1007\/978-3-540-30494-4_22"},{"key":"134_CR13","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous? In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904). Lecture Notes in Computer Science, vol. 2988, pp. 451\u2013466 (2004)","DOI":"10.1007\/978-3-540-24730-2_34"},{"key":"134_CR14","unstructured":"IBM Haifa.: CNF Benchmarks from IBM Formal Verification Benchmarks Library (2007)"},{"key":"134_CR15","unstructured":"Heimdahl, M., Rayadurgam, S. Visser, W., Devaraj, G., Gao, J.: Auto-generating test sequences using model checkers: a case study. In: Proceedings of the Third International Workshop on Formal Approaches to Testing of Software (FATES\u201903). Lecture Notes in Computer Science, vol. 2931, pp. 42\u201359 (2003)"},{"key":"134_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL\u201904), pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"issue":"2","key":"134_CR17","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"134_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. In: Proceedings of the 8th advanced research working conference on correct hardware design and verification methods (CHARME\u201999). Lecture Notes in Computer Science, vol. 1703, pp. 82\u201396 (1999)","DOI":"10.1007\/3-540-48153-2_8"},{"key":"134_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Interpolation and SAT-based model checking. In: Proceedings of the 15th International Conference on Computer Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 1\u201313 (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"134_CR20","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV\u201904). Lecture Notes in Computer Science, vol. 3114, pp. 57\u201369 (2004)","DOI":"10.1007\/978-3-540-27813-9_5"},{"key":"134_CR21","doi-asserted-by":"crossref","unstructured":"Purandare, M., Somenzi, F.: Vacuum cleaning CTL formulae. In: Proceedings of the 14th International Conference on Computer Aided Verification (CAV\u201902). Lecture Notes in Computer Science, vol. 2404, pp. 485\u2013499 (2002)","DOI":"10.1007\/3-540-45657-0_39"},{"issue":"1\u20132","key":"134_CR22","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman B., Mitchell D., Levesque H.: Generating hard satisfiability problems. Artif. Intell. 81(1\u20132), 17\u201329 (1996)","journal-title":"Artif. Intell."},{"key":"134_CR23","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: Proceedings of the 18th International Conference on Automated Software Engineering (ASE\u201903), pp. 94\u2013105, October (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"key":"134_CR24","doi-asserted-by":"crossref","unstructured":"Simmonds, J., Davies, J., Gurinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201907) (2007)","DOI":"10.1109\/FAMCAD.2007.16"},{"key":"134_CR25","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"134_CR26","doi-asserted-by":"crossref","unstructured":"Zarpas, E.: Benchmarking SAT solvers for bounded model checking. In: Proceedings of the 8th International Symposium on the Theory and Applications of Satisfiability Testing (SAT\u201905). Lecture Notes in Computer Science, vol. 3569, pp. 340\u2013354 (2005)","DOI":"10.1007\/11499107_25"},{"key":"134_CR27","unstructured":"Zhang, L., Fu, Z.: Boolean Satisfiability Research Group at Princeton. http:\/\/www.princeton.edu\/~chaff\/ , September (2006)"},{"key":"134_CR28","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the International Conference and Exposition on Design, Automation and Test in Europe (DATE\u201903), pp. 10880\u201310885 (2003)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0134-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0134-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0134-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:26Z","timestamp":1559114726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0134-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,6]]},"references-count":28,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["134"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0134-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1,6]]}}}