{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:44Z","timestamp":1725511904832},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540712084"},{"type":"electronic","value":"9783540712091"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_29","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T22:56:34Z","timestamp":1183589794000},"page":"373-388","source":"Crossref","is-referenced-by-count":8,"title":["Abstraction Refinement of Linear Programs with Arrays"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Benerecetti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacopo","family":"Mantovani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods and Software Engineering","author":"A. Armando","year":"2004","unstructured":"Armando, A., Castellini, C., Mantovani, J.: Software model checking using linear constraints. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, Springer, Heidelberg (2004)"},{"key":"29_CR2","series-title":"ENTCS","volume-title":"SoftMC\u201905","author":"A. Armando","year":"2005","unstructured":"Armando, A., Benerecetti, M., Mantovani, J.: Model checking linear programs with arrays. In: SoftMC\u201905. ENTCS, vol.\u00a0144, Elsevier, Amsterdam (2005)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"29_CR4","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. Henzinger","year":"2003","unstructured":"Henzinger, T., et al.: Software Verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"29_CR5","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL\u201904","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., et al.: Abstractions from proofs. In: POPL\u201904, Venice, Italy, pp. 232\u2013244. ACM Press, New York (2004), doi:10.1145\/964001.964021"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., et al.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"29_CR8","first-page":"368","volume-title":"Proc. of DAC 2003","author":"D. Kroening","year":"2003","unstructured":"Kroening, D., Clarke, E., Yorav, K.: Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. In: Proc. of DAC 2003, pp. 368\u2013371. ACM Press, New York (2003)"},{"key":"29_CR9","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"29_CR10","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/199448.199462","volume-title":"Proc. of POPL \u201995","author":"T. Reps","year":"1995","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proc. of POPL \u201995, San Francisco, California, United States, pp. 49\u201361. ACM Press, New York (1995)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45789-5_17","volume-title":"Static Analysis","author":"R. Bagnara","year":"2002","unstructured":"Bagnara, R., et al.: Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 213\u2013229. Springer, Heidelberg (2002)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","first-page":"515","volume-title":"Computer Aided Verification","author":"S. Berezin","year":"2004","unstructured":"Berezin, S., Barrett, C.W.: CVC Lite: A New Implementation of the Cooperating Validity Checker Category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"29_CR13","unstructured":"Black, P.E.: Gray code, in dictionary of algorithms and data structures (2005), http:\/\/www.nist.gov\/dads\/HTML\/graycode.html"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., et al.: Lazy abstraction. In: POPL 2002, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"}],"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-71209-1_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T21:20:59Z","timestamp":1683926459000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_29","relation":{},"subject":[]}}