{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:41:21Z","timestamp":1742391681240},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,2,24]],"date-time":"2005-02-24T00:00:00Z","timestamp":1109203200000},"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":[[2005,4]]},"DOI":"10.1007\/s10009-004-0169-2","type":"journal-article","created":{"date-parts":[[2005,2,23]],"date-time":"2005-02-23T12:49:53Z","timestamp":1109162993000},"page":"143-155","source":"Crossref","is-referenced-by-count":15,"title":["Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure"],"prefix":"10.1007","volume":"7","author":[{"given":"Bing","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,2,24]]},"reference":[{"key":"169_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Bjesse P, E\u00e9n N (2000) Symbolic reachability analysis based on SAT-solvers. In: 6th international conference on tools and algorithms for the construction of systems (TACAS). Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 411\u2013425","DOI":"10.1007\/3-540-46419-0_28"},{"key":"169_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"Alpern","year":"1985","unstructured":"Alpern B, Schneider FB (1985) Defining liveness. Inf Process Lett 21:181\u2013185","journal-title":"Inf Process Lett"},{"key":"169_CR3","doi-asserted-by":"crossref","unstructured":"Brayton RK et al. (1996) VIS: A system for verification and synthesis. In: Henzinger T, Alur R (eds) 8th conference on computer-aided verification (CAV\u201996). Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 428\u2013432","DOI":"10.1007\/3-540-61474-5_95"},{"key":"169_CR4","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: 5th international conference on tools and algorithms for construction and analysis of systems (TACAS\u201999), Amsterdam, The Netherlands, March 1999. Lecture notes in computer science, vol 1579. Springer, Berlin Heidelberg New York, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"169_CR5","doi-asserted-by":"crossref","unstructured":"Barner S, Geist D, Gringauze A (2002) Symbolic localization reduction with reconstruction layering and backtracking. In: Brinksma E, Larsen KG (eds) 14th conference on computer-aided verification (CAV 2002), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 65\u201377","DOI":"10.1007\/3-540-45657-0_6"},{"key":"169_CR6","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Kuehlmann A, Abraham J (2002) Property checking via structural analysis. In: Brinksma E, Larsen KG (eds) 14th conference on computer-aided verification (CAV\u201902), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 151\u2013165","DOI":"10.1007\/3-540-45657-0_12"},{"key":"169_CR7","doi-asserted-by":"crossref","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35(8):677\u2013691","DOI":"10.1109\/TC.1986.1676819"},{"key":"169_CR8","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by constructions or approximation of fixpoints. In: Proceedings of the ACM symposium on the principles of programming languages, pp 238\u2013250","DOI":"10.1145\/512950.512973"},{"key":"169_CR9","doi-asserted-by":"crossref","unstructured":"Chauhan P, Clarke E, Kukula J, Sapra S, Veith H, Wang D (2002) Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard MD, O\u2019Leary JW (eds) Formal methods in computer aided design, November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 33\u201351","DOI":"10.1007\/3-540-36126-X_3"},{"key":"169_CR10","doi-asserted-by":"crossref","unstructured":"Clarke E, Gupta A, Kukula J, Strichman O (2002) SAT based abstraction-refinement using ILP and machine learning. In: Brinksma E, Larsen KG (eds) 14th conference on computer-aided verification (CAV 2002), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 265\u2013279","DOI":"10.1007\/3-540-45657-0_20"},{"key":"169_CR11","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"169_CR12","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) Temporal induction by incremental SAT solving. In: 1st international workshop on bounded model checking. Electronic notes in theoretical computer science, 89(4). http:\/\/www.elsevier.nl\/locate\/entcs\/","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"169_CR13","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2003) Verification of proofs of unsatisfiability for CNF formulas. In: Design, automation and test in Europe (DATE\u201903), Munich, Germany, March 2003, pp 886\u2013891","DOI":"10.1109\/DATE.2003.1253718"},{"key":"169_CR14","doi-asserted-by":"crossref","unstructured":"Kr\u00f6ning D, Strichman O (2003) Efficient computation of recurrence diameters. In: 4th international conference on verification, model checking, and abstract interpretation, January 2003. Lecture notes in computer science, vol 2575. Springer, Berlin Heidelberg New York, pp 298\u2013309","DOI":"10.1007\/3-540-36384-X_24"},{"key":"169_CR15","doi-asserted-by":"crossref","unstructured":"Kurshan RP (1994) Computer-aided verification of coordinating processes. Princeton University Press, Princeton, NJ","DOI":"10.1515\/9781400864041"},{"key":"169_CR16","doi-asserted-by":"crossref","unstructured":"McMillan KL, Amla N (2003) Automatic abstraction without counterexamples. In: International conference on tools and algorithms for construction and analysis of systems (TACAS\u201903), Warsaw, Poland, April 2003. Lecture notes in computer science, vol 2619. Springer, Berlin Heidelberg New York, pp 2\u201317","DOI":"10.1007\/3-540-36577-X_2"},{"key":"169_CR17","doi-asserted-by":"crossref","unstructured":"McMillan KL (1994) Symbolic model checking. Kluwer, Boston","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"169_CR18","doi-asserted-by":"crossref","unstructured":"McMillan KL (2002) Applying SAT methods in unbounded symbolic model checking. In: Brinksma E, Larsen KG (eds) 14th conference on computer-aided verification (CAV\u201902), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"169_CR19","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr, Somenzi F (eds) 15th conference on computer-aided verification (CAV\u201903), July 2003. Lecture notes in computer science, vol 2725. Springer, Berlin Heidelberg New York, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"169_CR20","unstructured":"Milner R (1971) An algebraic definition of simulation between programs. In: Proceedings of the 2nd international joint conference on artificial intelligence, pp 481\u2013489"},{"key":"169_CR21","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver. In: Proceedings of the design automation conference, Las Vegas, June 2001, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"169_CR22","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt WA Jr, Johnson SD (eds) Formal methods in computer-aided design, November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"169_CR23","doi-asserted-by":"crossref","unstructured":"Williams P, Biere A, Clarke EM, Gupta A (2000) Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: Emerson EA, Sistla AP (eds) 12th conference on computer-aided verification (CAV\u201900), July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 124\u2013138","DOI":"10.1007\/10722167_13"},{"key":"169_CR24","doi-asserted-by":"crossref","unstructured":"Wang D, Ho P-H, Long J, Kukula J, Zhu Y, Ma T, Damiano R (2001) Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Proceedings of the design automation conference, Las Vegas, June 2001, pp 35\u201340","DOI":"10.1145\/378239.378260"},{"key":"169_CR25","doi-asserted-by":"crossref","unstructured":"Whittemore J, Kim J, Sakallah K (2001) SATIRE: A new incremental satisfiability engine. In: Proceedings of the design automation conference, Las Vegas, June 2001, pp 542\u2013545","DOI":"10.1145\/378239.379019"},{"key":"169_CR26","unstructured":"Wang C, Li B, Jin H, Hachtel GD, Somenzi F (2003) Improving Ariadne\u2019s bundle by following multiple threads in abstraction refinement. In: Proceedings of the international conference on computer-aided design, November 2003, pp 408\u2013415"},{"key":"169_CR27","unstructured":"Zhang L, Malik S (2003) Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Design, automation and test in Europe (DATE\u201903), Munich, Germany, March 2003, pp 880\u2013885"}],"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-004-0169-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0169-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0169-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T21:53:44Z","timestamp":1586123624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0169-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2,24]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["169"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0169-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2,24]]}}}