{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:17:06Z","timestamp":1762460226161},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415901"},{"type":"electronic","value":"9783319415918"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41591-8_8","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T13:27:27Z","timestamp":1466688447000},"page":"104-120","source":"Crossref","is-referenced-by-count":0,"title":["Combining Predicate Abstraction with Fixpoint Approximations"],"prefix":"10.1007","author":[{"given":"Tuba","family":"Yavuz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"8_CR1","volume-title":"Concurrent Programming: Principles and Practice","author":"GR Andrews","year":"1991","unstructured":"Andrews, G.R.: Concurrent Programming: Principles and Practice. Benjamin-Cummings Publishing Co., Inc., Redwood City (1991)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"T Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"issue":"5","key":"8_CR4","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM 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":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-45069-6_14","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Talupur, M., Wang, D.: Making predicate abstraction effcient: how to eliminate redundant predicates. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 126\u2013140. Springer, Heidelberg (2003)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysisof programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)","DOI":"10.1145\/512950.512973"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/3-540-45657-0_3","volume-title":"Computer Aided Verification","author":"P Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: On abstraction in software verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 37\u201356. Springer, Heidelberg (2002)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, pp. 84\u201396, January 1978","DOI":"10.1145\/512760.512770"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"6","key":"8_CR10","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/s10009-010-0162-x","volume":"12","author":"A Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Combining predicate and numeric abstraction for software model checking. STTT 12(6), 409\u2013427 (2010)","journal-title":"STTT"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"8_CR12","unstructured":"Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The omega library interface guide. Technical report, University of Maryland at College Park, College Park, MD, USA (1995)"},{"issue":"1","key":"8_CR13","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6(1), 11\u201344 (1995)","journal-title":"Form. Methods Syst. Des."},{"key":"8_CR14","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.: Principles of Program Analysis. Springer-Verlag New York Inc., Secaucus (1999)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3), May 2007","DOI":"10.1145\/1232420.1232422"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/978-3-642-05089-3_7","volume-title":"FM 2009: Formal Methods","author":"S Tonetta","year":"2009","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 89\u2013105. Springer, Heidelberg (2009)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-45988-X_6","volume-title":"Frontiers of Combining Systems","author":"T Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Heuristics for efficient manipulation of composite constraints. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 57\u201371. Springer, Heidelberg (2002)"},{"issue":"3","key":"8_CR18","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10703-009-0081-1","volume":"35","author":"T Yavuz-Kahveci","year":"2009","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Action language verifier: an infinite-state model checker for reactive software specifications. Formal Methods Syst. Des. 35(3), 325\u2013367 (2009)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:57:25Z","timestamp":1498309045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}