{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:07Z","timestamp":1776316927269,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439974","type":"print"},{"value":"9783540456575","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_20","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:59:43Z","timestamp":1179572383000},"page":"265-279","source":"Crossref","is-referenced-by-count":80,"title":["SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques"],"prefix":"10.1007","author":[{"given":"Edmund","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Anubhav","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"James","family":"Kukula","sequence":"additional","affiliation":[]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"F. Balarin and A. Sangiovanni-Vinventelli. An iterative approah to language containment. In C. Courcoubetis, editor, Proc. 5 th Intl. Conference on Computer Aided Verification (CAV\u201994), volume 697 of Lect. Notes in Comp. Sci., pages 29\u201340. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_4"},{"key":"20_CR2","unstructured":"M. Berkelaar. lpsolve, version 2.0. Eindhoven Univ. Tech., The Netherlands."},{"key":"20_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), LNCS. Springer-Verlag, 1999."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. Int. Journal of Software Tools for Technology Transfer (STTT), 1998.","DOI":"10.1007\/3-540-48683-6_44"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E. A. Emerson and A. P. Sistla, editors, Proc. 12th Intl. Conference on Computer Aided Verification (CAV\u201900), volume 1855 of Lect. Notes in Comp. Sci. Springer-Verlag, 2000.","DOI":"10.1007\/10722167_15"},{"issue":"5","key":"20_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans. Prog. Lang. Sys., 16(5):1512\u20131542, 1994.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"20_CR7","unstructured":"Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, 2001. June 2001, Boston, USA."},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer aided verification of coordinating processes. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"J. Lind-Nielsen and H. Andersan. Stepwise CTL model checking of state\/event systems. In N. Halbwachs and D. Peled, editors, Proc. 11th Intl. Conference on Computer Aided Verification (CAV\u201999), volume 1633 of Lect. Notes in Comp. Sci., pages 316\u2013327. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48683-6_28"},{"key":"20_CR10","unstructured":"Tom M. Mitchell. Machine Learning. WCB\/McGraw-Hill, 1997."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. Design Automation Conference 2001 (DAC\u201901), 2001.","DOI":"10.1145\/378239.379017"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"J. R. Quinlan. Induction of decision trees. Machine Learning, 1986.","DOI":"10.1007\/BF00116251"},{"key":"20_CR13","volume-title":"C4.5: Programs for Machine Learning","author":"J. R. Quinlan","year":"1993","unstructured":"J. R. Quinlan. C4.5: Programs for Machine Learning. Morgan Kaufmann, San Mateo, CA, 1993."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Dong Wang, Pei-Hsin Ho, Jiang Long, James Kukula, Yunshan Zhu, Tony Ma, and Robert Damiano. Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In Proc. Design Automation Conference 2001 (DAC\u201901), 2001.","DOI":"10.1145\/378239.378260"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:20:59Z","timestamp":1556414459000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}