{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:05:37Z","timestamp":1767337537002},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662534120"},{"type":"electronic","value":"9783662534137"}],"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-662-53413-7_10","type":"book-chapter","created":{"date-parts":[[2016,8,30]],"date-time":"2016-08-30T07:57:11Z","timestamp":1472543831000},"page":"189-211","source":"Crossref","is-referenced-by-count":11,"title":["Exploiting Sparsity in Difference-Bound Matrices"],"prefix":"10.1007","author":[{"given":"Graeme","family":"Gange","sequence":"first","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[]},{"given":"Harald","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,31]]},"reference":[{"key":"10_CR1","unstructured":"Competition on software verification (SV-COMP) (2016). http:\/\/sv-comp.sosy-lab.org\/2016\/ . Benchmarks https:\/\/github.com\/sosy-lab\/sv-benchmarks\/c . Accessed 30 Mar 2016"},{"issue":"1\u20134","key":"10_CR2","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1145\/176454.176484","volume":"2","author":"P Briggs","year":"1993","unstructured":"Briggs, P., Torczon, L.: An efficient representation for sparse sets. ACM Lett. Program. Lang. Syst. 2(1\u20134), 59\u201369 (1993)","journal-title":"ACM Lett. Program. Lang. Syst."},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/978-3-319-12736-1_16","volume-title":"Programming Languages and Systems","author":"A Chawdhary","year":"2014","unstructured":"Chawdhary, A., Robbins, E., King, A.: Simple and efficient algorithms for octagons. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 296\u2013313. Springer, Heidelberg (2014)"},{"issue":"2","key":"10_CR4","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"BV Cherkassky","year":"1999","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. Math. Program. 85(2), 277\u2013311 (1999)","journal-title":"Math. Program."},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/11814948_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S Cotton","year":"2006","unstructured":"Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170\u2013183. Springer, Heidelberg (2006)"},{"key":"10_CR6","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 Fourth ACM Symposium Principles of Programming Languages, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth ACM Symposium Principles of Programming Languages, pp. 269\u2013282. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"issue":"3","key":"10_CR8","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does Astr\u00e9e scale up? Formal Methods Syst. Des. 35(3), 229\u2013264 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Proceedings of the Fifth ACM Symposium Principles of Programming Languages, pp. 84\u201397. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Feydy, T., Schutt, A., Stuckey, P.J.: Global difference constraint propagation for finite domain solvers. In: Proceedings of the 10th International ACM SIGPLAN Conference Principles and Practice of Declarative Programming, pp. 226\u2013235. ACM Press (2008)","DOI":"10.1145\/1389449.1389478"},{"key":"10_CR12","volume-title":"Flows in Networks","author":"LR Ford","year":"1962","unstructured":"Ford, L.R., Fulkerson, D.R.: Flows in Networks. Princeton University Press, Princeton (1962)"},{"issue":"1","key":"10_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/321992.321993","volume":"24","author":"DB Johnson","year":"1977","unstructured":"Johnson, D.B.: Efficient algorithms for shortest paths in sparse networks. J. ACM 24(1), 1\u201313 (1977)","journal-title":"J. ACM"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Proceedings of the 18th International Symposium Real-Time Systems, pp. 14\u201324. IEEE Computer Society (1997)","DOI":"10.1109\/REAL.1997.641265"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceedings of the International Symposium Code Generation and Optimization (CGO 2004), pp. 75\u201386. IEEE Computer Society (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Proceedings of the 2008 ACM Symposium Applied Computing, pp. 184\u2013188. ACM Press (2008)","DOI":"10.1145\/1363686.1363736"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"issue":"1","key":"10_CR18","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Ord. Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Ord. Symbolic Comput."},{"key":"10_CR19","unstructured":"Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Notes of the ACM SIGPLAN Workshop on ML, pp. 77\u201386, September 1998"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: Making numerical program analysis fast. In: Proceedings of the 36th ACM SIGPLAN Conference Programming Language Design and Implementation, pp. 303\u2013313. ACM (2015)","DOI":"10.1145\/2813885.2738000"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the 25th ACM SIGPLAN Conference Programming Language Design and Implementation, pp. 231\u2013242. ACM Press (2004)","DOI":"10.1145\/996893.996869"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/978-3-642-31424-7_15","volume-title":"Computer Aided Verification","author":"AJ Venet","year":"2012","unstructured":"Venet, A.J.: The gauge domain: scalable analysis of linear inequality invariants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 139\u2013154. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-53413-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T22:20:04Z","timestamp":1568326804000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-53413-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662534120","9783662534137"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-53413-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}