{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:56:47Z","timestamp":1770296207825,"version":"3.49.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,9,19]],"date-time":"2013-09-19T00:00:00Z","timestamp":1379548800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10515-013-0132-0","type":"journal-article","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T15:14:40Z","timestamp":1379517280000},"page":"225-285","source":"Crossref","is-referenced-by-count":2,"title":["Counterexample-guided abstraction refinement for linear programs with arrays"],"prefix":"10.1007","volume":"21","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","published-online":{"date-parts":[[2013,9,19]]},"reference":[{"key":"132_CR1","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":"132_CR2","volume-title":"24th International Conference on Computer Aided Verification (CAV)","author":"F. Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Safari: SMT-based abstraction for arrays with interpolants. In: 24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA. Springer, Berlin (2012)"},{"key":"132_CR3","unstructured":"Aristotle Research Group, Georgia Institute of Technology. TCAS (1994). Available at http:\/\/www.cc.gatech.edu\/aristotle\/Tools\/subjects"},{"key":"132_CR4","series-title":"LNCS","volume-title":"ICFEM\u201904","author":"A. Armando","year":"2004","unstructured":"Armando, A., Castellini, C., Mantovani, J.: Software model checking using linear constraints. In: ICFEM\u201904, Seattle, USA. LNCS, vol.\u00a03308. Springer, Berlin (2004)"},{"key":"132_CR5","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, Edinburgh, UK. ENTCS, vol.\u00a0144. Elsevier, Amsterdam (2005)"},{"key":"132_CR6","series-title":"LNCS","volume-title":"SPIN","author":"A. Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: SPIN, Vienna, Austria. LNCS, vol.\u00a03925. Springer, Berlin (2006)"},{"key":"132_CR7","series-title":"LNCS","volume-title":"TACAS","author":"A. Armando","year":"2007","unstructured":"Armando, A., Benerecetti, M., Mantovani, J.: Abstraction refinement of linear programs with arrays. In: TACAS, Braga, Portugal. LNCS, vol.\u00a04424. Springer, Berlin (2007)"},{"key":"132_CR8","series-title":"LNCS","first-page":"213","volume-title":"SAS\u201902","author":"R. Bagnara","year":"2002","unstructured":"Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS\u201902, Madrid, Spain. LNCS, vol.\u00a02477, pp.\u00a0213\u2013229. Springer, Berlin (2002)"},{"key":"132_CR9","first-page":"113","volume-title":"Proc. of SPIN","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for Boolean programs. In: Proc. of SPIN, Stanford, USA, vol.\u00a01885, pp.\u00a0113\u2013130. Springer, Berlin (2000)"},{"key":"132_CR10","first-page":"103","volume-title":"Proc. of SPIN","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Proc. of SPIN, Toronto, Canada, pp.\u00a0103\u2013122. Springer, Berlin (2001)"},{"key":"132_CR11","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/1217935.1217943","volume-title":"EuroSys \u201906: Proceedings of the 2006 EuroSys Conference","author":"T. Ball","year":"2006","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys \u201906: Proceedings of the 2006 EuroSys Conference, New York, NY, USA, pp.\u00a073\u201385. ACM Press, New York (2006)"},{"key":"132_CR12","first-page":"515","volume-title":"CAV","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: a new implementation of the cooperating validity checker. In: CAV, vol.\u00a03114, pp.\u00a0515\u2013518. Springer, Boston (2004)"},{"key":"132_CR13","series-title":"LNCS","first-page":"64","volume-title":"Proceedings of CAV 2009","author":"G. Basler","year":"2009","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Proceedings of CAV 2009. LNCS, vol.\u00a05643, pp.\u00a064\u201378. Springer, Berlin (2009)"},{"key":"132_CR14","first-page":"184","volume-title":"CAV","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAChecker: a tool for configurable software verification. In: CAV, pp.\u00a0184\u2013190 (2011)"},{"key":"132_CR15","first-page":"25","volume-title":"FMCAD","author":"D. Beyer","year":"2009","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp.\u00a025\u201332 (2009)"},{"key":"132_CR16","first-page":"189","volume-title":"FMCAD","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD, pp.\u00a0189\u2013197 (2010)"},{"key":"132_CR17","unstructured":"Black, P.E.: Gray code, in dictionary of algorithms and data structures (2005). http:\/\/www.nist.gov\/dads\/HTML\/graycode.html"},{"issue":"1","key":"132_CR18","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1147\/sj.41.0025","volume":"4","author":"J. Bresenham","year":"1965","unstructured":"Bresenham, J.: Algorithm for computer control of a digital plotter. IBM Syst. J. 4(1), 25\u201330 (1965)","journal-title":"IBM Syst. J."},{"issue":"8","key":"132_CR19","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"132_CR20","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Trans. Program. Lang. Syst. 21(4), 747\u2013789 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"132_CR21","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000040026.56959.91","volume":"25","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. Form. Methods Syst. Des. 25, 129\u2013166 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"132_CR22","first-page":"235","volume-title":"ACM Conference on Computer and Communications Security","author":"H. Chen","year":"2002","unstructured":"Chen, H., Wagner, D.: Mops: an infrastructure for examining security properties of software. In: ACM Conference on Computer and Communications Security, Washington, USA, pp.\u00a0235\u2013244. ACM, New York (2002)"},{"key":"132_CR23","series-title":"LNCS","first-page":"3","volume-title":"Proceedings of the Sixth Asian Symposium (APLAS\u201908)","author":"L. Chen","year":"2009","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A\u00a0sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) Proceedings of the Sixth Asian Symposium (APLAS\u201908), Bangalore, India, 17\u201319 January 2009. LNCS, vol.\u00a05356, pp.\u00a03\u201318. Springer, Berlin (2009)"},{"key":"132_CR24","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E.: Model Checking. MIT Press, Boston (2000)"},{"key":"132_CR25","series-title":"LNCS","first-page":"154","volume-title":"CAV","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV, Chicago, USA. LNCS, vol.\u00a01855, pp.\u00a0154\u2013169. Springer, Berlin (2000)"},{"key":"132_CR26","series-title":"LNCS","first-page":"570","volume-title":"TACAS","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, Edinburgh, UK. LNCS, vol.\u00a03440, pp.\u00a0570\u2013574. Springer, Berlin (2005)"},{"key":"132_CR27","first-page":"142","volume-title":"ESEC\/SIGSOFT FSE","author":"A. Coen-Porisini","year":"2001","unstructured":"Coen-Porisini, A., Denaro, G., Ghezzi, C., Pezz\u00e8, M.: Using symbolic execution for verifying safety-critical systems. In: ESEC\/SIGSOFT FSE, Vienna, Austria, pp.\u00a0142\u2013151. ACM, New York (2001)"},{"key":"132_CR28","series-title":"LNCS","first-page":"182","volume-title":"TACAS","author":"H. Collavizza","year":"2006","unstructured":"Collavizza, H., Rueher, M.: Exploration of the capabilities of constraint programming for software verification. In: TACAS, Vienna, Austria. LNCS, vol.\u00a03920, pp.\u00a0182\u2013196. Springer, Berlin (2006)"},{"key":"132_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/11513988_30","volume-title":"CAV","author":"B. Cook","year":"2005","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV. Lecture Notes in Computer Science, vol.\u00a03576, pp.\u00a0296\u2013300. Springer, Berlin (2005)"},{"key":"132_CR30","series-title":"LNCS","first-page":"137","volume-title":"ASE","author":"L. Cordeiro","year":"2009","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: ASE. LNCS, pp.\u00a0137\u2013148. IEEE Computer Society, Los Alamitos (2009)"},{"key":"132_CR31","first-page":"238","volume-title":"POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, Los Angeles, USA, pp.\u00a0238\u2013252. ACM, New York (1977)"},{"key":"132_CR32","first-page":"84","volume-title":"POPL","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) POPL, pp.\u00a084\u201396. ACM Press, New York (1978)"},{"key":"132_CR33","first-page":"105","volume-title":"POPL","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A\u00a0parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp.\u00a0105\u2013118 (2011)"},{"key":"132_CR34","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Technical Report 148, HP Labs (2003)"},{"key":"132_CR35","series-title":"LNCS","first-page":"324","volume-title":"Proc. of CAV","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Proc. of CAV, Paris, France. LNCS, vol.\u00a02102, pp.\u00a0324\u2013336. Springer, Berlin (2001)"},{"key":"132_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1007\/978-3-642-36742-7_48","volume-title":"TACAS","author":"S. Falke","year":"2013","unstructured":"Falke, S., Merz, F., Sinz, C.: Llbmc: improved bounded model checking of C programs using LLVM (competition contribution). In: Smolka, S.A., Piterman, N. (eds.) TACAS. Lecture Notes in Computer Science, vol.\u00a07795, pp.\u00a0623\u2013626. Springer, Berlin (2013)"},{"key":"132_CR37","series-title":"LNCS","first-page":"189","volume-title":"Proc. of ESOP","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C.: Automatic software model checking using CLP. In: Proc. of ESOP, Warsaw, Poland. LNCS, vol.\u00a02618, pp.\u00a0189\u2013203. Springer, Berlin (2003)"},{"issue":"1\u20133","key":"132_CR38","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.scico.2004.01.006","volume":"50","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C.: Automatic software model checking via constraint logic. Sci. Comput. Program. 50(1\u20133), 253\u2013270 (2004a)","journal-title":"Sci. Comput. Program."},{"key":"132_CR39","volume-title":"CP+CV\u201904","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C.: Software model checking via iterative abstraction refinement of constraint logic queries. In: CP+CV\u201904 (2004b)"},{"key":"132_CR40","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI \u201902: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI \u201902: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation New York, NY, USA, pp.\u00a0234\u2013245. ACM Press, New York (2002)"},{"key":"132_CR41","first-page":"338","volume-title":"POPL","author":"D. Gopan","year":"2005","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL, pp.\u00a0338\u2013350 (2005)"},{"key":"132_CR42","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1145\/1375581.1375623","volume-title":"PLDI","author":"N. Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp.\u00a0339\u2013348 (2008)"},{"key":"132_CR43","series-title":"LNCS","first-page":"526","volume-title":"CAV","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: CAV, Copenhagen, Denmark. LNCS, vol.\u00a02404, pp.\u00a0526\u2013538. Springer, Berlin (2002a)"},{"key":"132_CR44","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, Portland, USA, pp.\u00a058\u201370. ACM, New York (2002b)"},{"key":"132_CR45","series-title":"LNCS","first-page":"235","volume-title":"Proc. of SPIN","author":"T. Henzinger","year":"2003","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Proc. of SPIN. LNCS, vol.\u00a02648, pp.\u00a0235\u2013239. Springer, Berlin (2003)"},{"key":"132_CR46","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1109\/ICCD.2005.77","volume-title":"ICCD \u201905: Proceedings of the 2005 International Conference on Computer Design","author":"F. Ivanicic","year":"2005","unstructured":"Ivanicic, F., Shlyakhter, I., Gupta, A., Ganai, M.K.: Model checking C programs using F-soft. In: ICCD \u201905: Proceedings of the 2005 International Conference on Computer Design, Washington, DC, USA, pp.\u00a0297\u2013308. IEEE Computer Society, Los Alamitos (2005)"},{"key":"132_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1007\/978-3-540-31980-1_39","volume-title":"TACAS","author":"C.W. Keller","year":"2005","unstructured":"Keller, C.W., Saha, D., Basu, S., Smolka, S.A.: Focuscheck: a tool for model checking and debugging sequential C programs. In: TACAS, Edinburgh, UK. Lecture Notes in Computer Science, vol.\u00a03440, pp.\u00a0563\u2013569. Springer, Berlin (2005)"},{"key":"132_CR48","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, Anaheim, USA, pp.\u00a0368\u2013371. ACM Press, New York (2003)"},{"key":"132_CR49","unstructured":"McMillan, K.: Symbolic model checking: an approach to the state explosion problem. PhD thesis, Carnegie Mellon University (1992). Also available as CMU Technical Report CMU-CS-92-131"},{"key":"132_CR50","volume-title":"Proc. of POPL","author":"M. Mueller-Olm","year":"2004","unstructured":"Mueller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. of POPL, Venice, Italy. ACM Press, New York (2004)"},{"key":"132_CR51","volume-title":"OSDI","author":"M. Musuvathi","year":"2002","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. In: OSDI, Boston, USA. USENIX Association, Berkeley (2002)"},{"key":"132_CR52","volume-title":"PADL","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: PADL. Springer, Berlin (2007)"},{"key":"132_CR53","unstructured":"Radio Technical Commission for Aeronautics (RTCA), Inc.: Minimum operational performance standards for traffic alert and collision avoidance system II (TCAS II) airborne equipment. Document no. DO-185A (1997)"},{"key":"132_CR54","doi-asserted-by":"crossref","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, United States, pp.\u00a049\u201361. ACM Press, New York (1995)"},{"key":"132_CR55","unstructured":"Seoul National University, Real Time Research Group: SNU real time benchmarks. Available at http:\/\/archi.snu.ac.kr\/realtime\/benchmark"},{"key":"132_CR56","first-page":"234","volume":"8","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Zap. Nau\u010d. Semin. POMI 8, 234\u2013259 (1968). English translation of this volume: Consultants Bureau, N.Y., 1970, pp.\u00a0115\u2013125","journal-title":"Zap. Nau\u010d. Semin. POMI"},{"key":"132_CR57","series-title":"LNCS","first-page":"139","volume-title":"CAV","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Saturn: a SAT-based tool for bug detection. In: CAV, Edinburgh, UK. LNCS, vol.\u00a03576, pp.\u00a0139\u2013143. Springer, Berlin (2005)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-013-0132-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-013-0132-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-013-0132-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T23:18:57Z","timestamp":1715987937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-013-0132-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,19]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["132"],"URL":"https:\/\/doi.org\/10.1007\/s10515-013-0132-0","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,19]]}}}