{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:49:16Z","timestamp":1725504556616},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781622"},{"type":"electronic","value":"9783540781639"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_22","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"248-262","source":"Crossref","is-referenced-by-count":4,"title":["A Forward-Backward Abstraction Refinement Algorithm"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Ranzato","sequence":"first","affiliation":[]},{"given":"Olivia Rossi","family":"Doria","sequence":"additional","affiliation":[]},{"given":"Francesco","family":"Tapparo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM Project: Debugging system software via static analysis. In: Proc. 29th ACM POPL, pp. 1\u20133 (2002)","key":"22_CR1","DOI":"10.1145\/503272.503274"},{"issue":"6","key":"22_CR2","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., et al.: Modular verification of software components in C. IEEE Transactions on Software Engineering\u00a030(6), 388\u2013402 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR3","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-44577-3_12","volume-title":"Informatics","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., et al.: Progress on the State Explosion Problem in Model Checking. In: Wilhelm, R. (ed.) Dagstuhl Seminar 2000. LNCS, vol.\u00a02000, pp. 176\u2013194. Springer, Heidelberg (2001)"},{"issue":"5","key":"22_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., et al.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"unstructured":"Cousot, P.: M\u00e8thodes it\u00e8ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e8rateurs monotones sur un treillis, analyse s\u00e8mantique de programmes. PhD Thesis, Univ.de Grenoble, France (1978)","key":"22_CR6"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th ACM POPL, pp. 269\u2013282 (1979)","key":"22_CR7","DOI":"10.1145\/567752.567778"},{"issue":"2-3","key":"22_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Programming\u00a013(2-3), 103\u2013179 (1992)","journal-title":"J. Logic Programming"},{"issue":"1","key":"22_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Automated Software Engineering\u00a06(1), 69\u201395 (1999)","journal-title":"Automated Software Engineering"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-74061-2_21","volume-title":"Static Analysis","author":"P. Cousot","year":"2007","unstructured":"Cousot, P., Ganty, P., Raskin, J.-F.: Fixpoint-Guided Abstraction Refinements. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 333\u2013348. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"22_CR11","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"unstructured":"Ganty, P.: The Fixpoint Checking Problem: An Abstraction Refinement Perspective. PhD Thesis, Universit\u00e9 Libre de Bruxelles (2007)","key":"22_CR12"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11609773_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Ganty","year":"2005","unstructured":"Ganty, P., Raskin, J.F., Van Begin, L.: A Complete Abstract Interpretation Framework for Coverability Properties of  WSTS. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 49\u201364. Springer, Heidelberg (2005)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-73094-1_10","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"P. Ganty","year":"2007","unstructured":"Ganty, P., Raskin, J.F., Van Begin, L.: From Many Places to Few: Automatic Abstraction Refinement for Petri Nets. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol.\u00a04546, pp. 124\u2013143. Springer, Heidelberg (2007)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Rajamani, S.K.: Counterexample Driven Refinement for Abstract Interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., et al.: Lazy abstraction. In: Proc. 29th ACM POPL, pp. 58\u201370 (2002)","key":"22_CR16","DOI":"10.1145\/503272.503279"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., et al.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-71322-7_13","volume-title":"Program Analysis and Compilation, Theory and Practice","author":"R. Manevich","year":"2007","unstructured":"Manevich, R., et al.: Abstract Counterexample-Based Refinement for Powerset Domains. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol.\u00a04444, pp. 273\u2013292. Springer, Heidelberg (2007)"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44978-7_7","volume-title":"Programs as Data Objects","author":"D. Mass\u00e9","year":"2001","unstructured":"Mass\u00e9, D.: Combining Forward and Backward Analyses of Temporal Properties. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, Springer, Heidelberg (2001)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-540-31980-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Ranzato","year":"2005","unstructured":"Ranzato, F., Tapparo, F.: An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 140\u2013156. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:00:35Z","timestamp":1619521235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_22","relation":{},"subject":[]}}