{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T17:40:26Z","timestamp":1740937226959,"version":"3.38.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,2,17]],"date-time":"2011-02-17T00:00:00Z","timestamp":1297900800000},"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":[[2012,2]]},"DOI":"10.1007\/s10009-011-0185-y","type":"journal-article","created":{"date-parts":[[2011,2,16]],"date-time":"2011-02-16T10:45:59Z","timestamp":1297853159000},"page":"1-14","source":"Crossref","is-referenced-by-count":4,"title":["An abstraction refinement approach combining precise and approximated techniques"],"prefix":"10.1007","volume":"14","author":[{"given":"Natasha","family":"Sharygina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aliaksei","family":"Tsitovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,2,17]]},"reference":[{"key":"185_CR1","unstructured":"https:\/\/www.isc.org\/software\/inn"},{"key":"185_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining approximations in software predicate abstraction. In: TACAS 388\u2013403 (2004)","DOI":"10.1007\/978-3-540-24730-2_30"},{"key":"185_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 203\u2013213 (2001)","DOI":"10.1145\/381694.378846"},{"issue":"1","key":"185_CR4","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T. Ball","year":"2003","unstructured":"Ball T., Podelski A., Rajamani S.K.: Boolean and Cartesian abstraction for model checking C programs. STTT 5(1), 49\u201358 (2003)","journal-title":"STTT"},{"key":"185_CR5","unstructured":"Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical report 2000\u20132014, Microsoft research, February (2000)"},{"key":"185_CR6","unstructured":"Ball, T., Rajamani, S.K.: Generating abstract explanations of spurious counterexamples in C programs. Technical report 2002\u20132009, Microsoft research, September (2002)"},{"key":"185_CR7","doi-asserted-by":"crossref","unstructured":"Braghin, C., Sharygina, N., Barone-Adesi, K.: Automated verification of security policies in mobile code. In: Davies, J., Gibbons, J., (eds) IFM. volume 4591 of Lecture Notes in Computer Science. Springer, Berlin, pp. 37\u201353 (2007)","DOI":"10.1007\/978-3-540-73210-5_3"},{"issue":"8","key":"185_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant R. E.: Graph-based algorithms for boolean function manipulation. IEEE Trans Comput C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans Comput"},{"issue":"2","key":"185_CR9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"185_CR10","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Franz\u00e9n, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R. K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD IEEE, pp. 69\u201376 (2007)","DOI":"10.1109\/FAMCAD.2007.35"},{"key":"185_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: SAT (2003)","DOI":"10.1007\/978-3-540-24605-3_7"},{"key":"185_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: CAV, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"issue":"5","key":"185_CR13","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke E.M., Grumberg O., Long D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"185_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Gupta, A., Kukula, J.H., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: CAV, pp. 265\u2013279 (2002)","DOI":"10.1007\/3-540-45657-0_20"},{"issue":"2\u20133","key":"185_CR15","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E.M. Clarke","year":"2004","unstructured":"Clarke E.M., Kroening D., Sharygina N., Yorav K.: Predicate abstraction of ANSI-C programs using SAT. Formal methods in system design 25(2\u20133), 105\u2013127 (2004)","journal-title":"Formal methods in system design"},{"key":"185_CR16","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: CAV, pp. 293\u2013304 (1998)","DOI":"10.1007\/BFb0028753"},{"key":"185_CR17","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: LICS, pp. 51\u201360 (2001)","DOI":"10.1109\/LICS.2001.932482"},{"key":"185_CR18","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: CAV (1999)","DOI":"10.1007\/3-540-48683-6_16"},{"key":"185_CR19","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N., An extensible sat-solver. In: SAT, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"185_CR20","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"185_CR21","doi-asserted-by":"crossref","unstructured":"Gupta, A., Strichman, O.: Abstraction refinement for bounded model checking. In: CAV, pp. 112\u2013124 (2005)","DOI":"10.1007\/11513988_11"},{"key":"185_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"185_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"185_CR24","doi-asserted-by":"crossref","unstructured":"Jain, H., Kroening, D., Sharygina, N., Clarke, E.M.: Word level predicate abstraction and refinement for verifying RTL verilog. In: DAC, pp. 445\u2013450 (2005)","DOI":"10.21236\/ADA470547"},{"key":"185_CR25","doi-asserted-by":"crossref","unstructured":"Jain, H., Ivancic, F., Gupta, A., Ganai, M. K.: Localization and register sharing for predicate abstraction. In: TACAS, pp. 397\u2013412 (2005)","DOI":"10.1007\/978-3-540-31980-1_26"},{"key":"185_CR26","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: CAV, pp. 39\u201351 (2005)","DOI":"10.1007\/11513988_6"},{"key":"185_CR27","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: TACAS, pp. 459\u2013473 (2006)","DOI":"10.1007\/11691372_33"},{"key":"185_CR28","doi-asserted-by":"crossref","unstructured":"Ku, K., Hart, T. E., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: ASE \u201907 ACM Press, pp. 389\u2013392 (2007)","DOI":"10.1145\/1321631.1321691"},{"key":"185_CR29","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Ball, T., Cook, B.: Predicate abstraction via symbolic decision procedures. Log. Methods Comput. Sci. 3(2) (2007)","DOI":"10.2168\/LMCS-3(2:1)2007"},{"key":"185_CR30","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: CAV. LNCS, Springer, Berlin, pp. 424\u2013437 (2006)","DOI":"10.1007\/11817963_39"},{"key":"185_CR31","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: CAV, pp. 123\u2013136 (2006)","DOI":"10.1007\/11817963_14"},{"key":"185_CR32","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: CAV, pp. 250\u2013264 (2002)","DOI":"10.1007\/3-540-45657-0_19"},{"key":"185_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson F., Nielson H. R., Hankin C. L.: Principles of Program Analysis. Springer, Berlin (1999)"},{"key":"185_CR34","doi-asserted-by":"crossref","unstructured":"Sharygina, N., Tonetta, S., Tsitovich, A.: The synergy of precise and fast abstractions for program verification. In: 24th annual ACM symposium on applied computing. Honolulu, Hawaii, USA, ACM (2009)","DOI":"10.1145\/1529282.1529404"}],"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-011-0185-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0185-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0185-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T17:13:34Z","timestamp":1740935614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0185-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,2,17]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["185"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0185-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,2,17]]}}}