{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:26Z","timestamp":1725558986708},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_26","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:44:59Z","timestamp":1278888299000},"page":"397-412","source":"Crossref","is-referenced-by-count":9,"title":["Localization and Register Sharing for Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Himanshu","family":"Jain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malay K.","family":"Ganai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-540-24730-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 388\u2013403. Springer, Heidelberg (2004)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. Programming Language Design and Implementation, 203\u2013213 (2001)","DOI":"10.1145\/381694.378846"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 268. Springer, Heidelberg (2001)"},{"key":"26_CR4","volume-title":"SPIN Workshop on Model Checking of Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software. Springer, Heidelberg (2001)"},{"key":"26_CR5","first-page":"385","volume-title":"ICSE 2003","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE 2003, pp. 385\u2013395. IEEE, Los Alamitos (2003)"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI\u2013C programs using SAT. Formal Methods in System Design\u00a025, 105\u2013127 (2004)","journal-title":"Formal Methods in System Design"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. Journal of Symbolic Logic\u00a022, 250\u2013268 (1957)","journal-title":"Journal of Symbolic Logic"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"26_CR10","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)"},{"key":"26_CR11","first-page":"72","volume-title":"CAV 1997","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV 1997, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"26_CR12","unstructured":"Gupta, A., Ganai, M.K., Ashar, P., Yang, Z.: Iterative abstraction using SAT-based BMC with proof analysis. In: International Conference on Computer Aided Design (ICCAD) (2003)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"26_CR14","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL 2004","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"26_CR15","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. In: Symposium on Leveraging Applications of Formal Methods (2004)"},{"key":"26_CR16","first-page":"7","volume-title":"MEMOCODE 2004","author":"H. Jain","year":"2004","unstructured":"Jain, H., Kroening, D., Clarke, E.: Verification of SpecC using predicate abstraction. In: MEMOCODE 2004, pp. 7\u201316. IEEE, Los Alamitos (2004)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Rugina, R., Rinard, M.C.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In: PLDI 2000, pp. 182\u2013195 (2000)","DOI":"10.1145\/358438.349325"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-49059-0_13","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"V. Rusu","year":"1999","unstructured":"Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 178\u2013192. Springer, Heidelberg (1999)"},{"key":"26_CR21","unstructured":"Zaks, A., Ivan\u010di\u0107, F., Cadambi, H., Shlyakhter, I., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Range analysis for software verification (2005) (Submitted for publication)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:53:09Z","timestamp":1558295589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}