{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:22:59Z","timestamp":1752985379162},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642331244"},{"type":"electronic","value":"9783642331251"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_15","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T06:47:24Z","timestamp":1346222844000},"page":"198-213","source":"Crossref","is-referenced-by-count":23,"title":["When the Decreasing Sequence Fails"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Halbwachs","sequence":"first","affiliation":[]},{"given":"Julien","family":"Henry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, PLDI 2003, San Diego (Ca.), pp. 196\u2013207 (June 2003)","key":"15_CR1","DOI":"10.1145\/781131.781153"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S. Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition Systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic Model Checking of Infinite State Systems using Presburger Arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R. Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise Widening Operators for Convex Polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 337\u2013354. Springer, Heidelberg (2003)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Formal Methods in Programming and Their Applications","author":"F. Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Efficient Chaotic Iterations Strategies with Widening. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol.\u00a0735, pp. 128\u2013141. Springer, Heidelberg (1993)"},{"key":"15_CR6","volume-title":"2nd Int. Symp. on Programming","author":"P. Cousot","year":"1976","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Int. Symp. on Programming. Dunod, Paris (1976)"},{"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: 4th ACM Symposium on Principles of Programming Languages, POPL 1977, Los Angeles (January 1977)","key":"15_CR7","DOI":"10.1145\/512950.512973"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/11513988_46","volume-title":"Computer Aided Verification","author":"A. Costan","year":"2005","unstructured":"Costan, A., Gaubert, S., Goubault, \u00c9., Martel, M., Putot, S.: A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 462\u2013475. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5th ACM Symposium on Principles of Programming Languages, POPL 1978, Tucson, Arizona (January 1978)","key":"15_CR9","DOI":"10.1145\/512760.512770"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"issue":"1","key":"15_CR11","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.cl.2010.09.001","volume":"37","author":"A. Cortesi","year":"2011","unstructured":"Cortesi, A., Zanioli, M.: Widening and narrowing operators for abstract interpretation. Computer Languages, Systems & Structures\u00a037(1), 24\u201342 (2011)","journal-title":"Computer Languages, Systems & Structures"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11823230_10","volume-title":"Static Analysis","author":"L. Gonnord","year":"2006","unstructured":"Gonnord, L., Halbwachs, N.: Combining Widening and Acceleration in Linear Relation Analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 144\u2013160. Springer, Heidelberg (2006)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-47764-0_14","volume-title":"Static Analysis","author":"\u00c9. Goubault","year":"2001","unstructured":"Goubault, \u00c9.: Static Analyses of the Precision of Floating-Point Operations. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 234\u2013259. Springer, Heidelberg (2001)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead Widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D. Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided Static Analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 349\u2013365. Springer, Heidelberg (2007)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-540-71316-6_21","volume-title":"Programming Languages and Systems","author":"T. Gawlitza","year":"2007","unstructured":"Gawlitza, T., Seidl, H.: Precise Fixpoint Computation Through Strategy Iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 300\u2013315. Springer, Heidelberg (2007)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Delay Analysis in Synchronous Programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 333\u2013346. Springer, Heidelberg (1993)"},{"issue":"2","key":"15_CR18","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Formal Methods in System Design"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"15_CR20","first-page":"75","volume-title":"CGO 2004","author":"C. Lattner","year":"2004","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework fopr lifelong program analysis & transformation. In: CGO 2004, pp. 75\u201386. IEEE Computer Society, Washington, DC (2004)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-24372-1_38","volume-title":"Automated Technology for Verification and Analysis","author":"L. Lakhdar-Chaouch","year":"2011","unstructured":"Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with Thresholds for Programs with Complex Control Graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 492\u2013502. Springer, Heidelberg (2011)"},{"unstructured":"Min\u00e9, A.: Weakly relational numerical abstract domains. PhD thesis, Ecole Polytechnique (2004)","key":"15_CR22"},{"doi-asserted-by":"crossref","unstructured":"Monniaux, D., Le Guen, J.: Stratified static analysis based on variable dependencies. In: Third International Workshop on Numerical and Symbolic Abstract Domains, Venice (September 2011)","key":"15_CR23","DOI":"10.1016\/j.entcs.2012.10.008"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-24738-8_18","volume-title":"Numerical Software with Result Verification","author":"S. Putot","year":"2004","unstructured":"Putot, S., Goubault, \u00c9., Martel, M.: Static Analysis-Based Validation of Floating-Point Computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Numerical Software with Result Verification. LNCS, vol.\u00a02991, pp. 306\u2013313. Springer, Heidelberg (2004)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-Based Linear-Relations Analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 53\u201368. Springer, Heidelberg (2004)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable Analysis of Linear Systems Using Mathematical Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-24730-2_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z. Su","year":"2004","unstructured":"Su, Z., Wagner, D.: A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 280\u2013295. Springer, Heidelberg (2004)"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal on Computing\u00a01, 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-73368-3_40","volume-title":"Computer Aided Verification","author":"C. Wang","year":"2007","unstructured":"Wang, C., Yang, Z., Gupta, A., Ivan\u010di\u0107, F.: Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 352\u2013365. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:56:10Z","timestamp":1620129370000},"score":1,"resource":{"primary":{"URL":"https:\/\/linproxy.fan.workers.dev:443\/http\/link.springer.com\/10.1007\/978-3-642-33125-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":30,"URL":"https:\/\/linproxy.fan.workers.dev:443\/https\/doi.org\/10.1007\/978-3-642-33125-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}