{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:18:28Z","timestamp":1745986708185,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642358722"},{"type":"electronic","value":"9783642358739"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35873-9_25","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T06:22:57Z","timestamp":1357107777000},"page":"414-433","source":"Crossref","is-referenced-by-count":6,"title":["Logico-Numerical Max-Strategy Iteration"],"prefix":"10.1007","author":[{"given":"Peter","family":"Schrammel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavle","family":"Subotic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: a declarative language for real-time programming. In: Principles of Programming Languages, pp. 178\u2013188. ACM (1987)","key":"25_CR1","DOI":"10.1145\/41625.41641"},{"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: Principles of Programming Languages, pp. 238\u2013252 (1977)","key":"25_CR2","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages, pp. 84\u201397. ACM (1978)","key":"25_CR3","DOI":"10.1145\/512760.512770"},{"key":"25_CR4","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)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-71316-6_17","volume-title":"Programming Languages and Systems","author":"S. Gaubert","year":"2007","unstructured":"Gaubert, S., Goubault, \u00c9., Taly, A., Zennou, S.: Static Analysis by Policy Iteration on Relational Domains. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-11957-6_3","volume-title":"Programming Languages and Systems","author":"A. Adj\u00e9","year":"2010","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 23\u201342. Springer, Heidelberg (2010)"},{"key":"25_CR7","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":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-74915-8_6","volume-title":"Computer Science Logic","author":"T. Gawlitza","year":"2007","unstructured":"Gawlitza, T., Seidl, H.: Precise Relational Invariants Through Strategy Iteration. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 23\u201340. Springer, Heidelberg (2007)"},{"key":"25_CR9","doi-asserted-by":"publisher","first-page":"1416","DOI":"10.1016\/j.jsc.2011.12.048","volume":"47","author":"T. Gawlitza","year":"2012","unstructured":"Gawlitza, T., Seidl, H., Adj\u00e9, A., Gaubert, S., Goubault, E.: Abstract interpretation meets convex optimization. Journal of Symbolic Computation\u00a047, 1416\u20131446 (2012)","journal-title":"Journal of Symbolic Computation"},{"key":"25_CR10","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)"},{"unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Dunod, pp. 106\u2013130 (1976)","key":"25_CR11"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Working Conference on Reverse Engineering, pp. 310\u2013319. IEEE (2001)","key":"25_CR13","DOI":"10.1109\/WCRE.2001.957836"},{"key":"25_CR14","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":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-48294-6_3","volume-title":"Static Analysis","author":"B. Jeannet","year":"1999","unstructured":"Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic Partitioning in Analyses of Numerical Properties. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 39\u201350. Springer, Heidelberg (1999)"},{"issue":"5","key":"25_CR16","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1145\/780822.781153","volume":"38","author":"Bruno Blanchet","year":"2003","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: Programming Language Design and Implementation, pp. 196\u2013207. ACM (2003)","journal-title":"ACM SIGPLAN Notices"},{"doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of lustre programs with smt-based techniques. In: Formal Methods in Computer-Aided Design, pp. 1\u20139. IEEE (2008)","key":"25_CR17","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-68237-0_24","volume-title":"FM 2008: Formal Methods","author":"T. Gawlitza","year":"2008","unstructured":"Gawlitza, T., Seidl, H.: Precise Interval Analysis vs. Parity Games. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 342\u2013357. Springer, Heidelberg (2008)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-642-15769-1_17","volume-title":"Static Analysis","author":"T.M. Gawlitza","year":"2010","unstructured":"Gawlitza, T.M., Seidl, H.: Computing Relaxed Abstract Semantics w.r.t. Quadratic Zones Precisely. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 271\u2013286. Springer, Heidelberg (2010)"},{"key":"25_CR20","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1961204.1961207","volume":"33","author":"T.M. Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Seidl, H.: Solving systems of rational equations through strategy iteration. Transactions on Programming Languages and Systems\u00a033, 11 (2011)","journal-title":"Transactions on Programming Languages and Systems"},{"unstructured":"Jeannet, B.: BDDAPRON: A logico-numerical abstract domain library (2009), http:\/\/pop-art.inrialpes.fr\/~bjeannet\/bjeannet-forge\/bddapron\/","key":"25_CR21"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-24372-1_21","volume-title":"Automated Technology for Verification and Analysis","author":"P. Sotin","year":"2011","unstructured":"Sotin, P., Jeannet, B., V\u00e9drine, F., Goubault, E.: Policy Iteration within Logico-Numerical Abstract Domains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 290\u2013305. Springer, Heidelberg (2011)"},{"key":"25_CR23","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":"25_CR24","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1016\/j.jsc.2011.12.051","volume":"47","author":"P. Schrammel","year":"2012","unstructured":"Schrammel, P., Jeannet, B.: Applying abstract acceleration to (co-)reachability analysis of reactive programs. Journal of Symbolic Computation\u00a047, 1512\u20131532 (2012)","journal-title":"Journal of Symbolic Computation"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-23702-7_19","volume-title":"Static Analysis","author":"P. Schrammel","year":"2011","unstructured":"Schrammel, P., Jeannet, B.: Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 233\u2013248. Springer, Heidelberg (2011)"},{"key":"25_CR26","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.W.: Guided Static Analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 349\u2013365. Springer, Heidelberg (2007)"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-642-24372-1_36","volume-title":"Automated Technology for Verification and Analysis","author":"T. Dang","year":"2011","unstructured":"Dang, T., Gawlitza, T.M.: Discretizing Affine Hybrid Automata with Uncertainty. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 473\u2013481. Springer, Heidelberg (2011)"},{"key":"25_CR28","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)"},{"doi-asserted-by":"crossref","unstructured":"Schrammel, P., Jeannet, B.: From hybrid data-flow languages to hybrid automata: A complete translation. In: Hybrid Systems: Computation and Control, pp. 167\u2013176. ACM (2012)","key":"25_CR29","DOI":"10.1145\/2185632.2185658"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-25318-8_6","volume-title":"Programming Languages and Systems","author":"T. Dang","year":"2011","unstructured":"Dang, T., Gawlitza, T.M.: Template-Based Unbounded Time Verification of Affine Hybrid Automata. In: Yang, H. (ed.) APLAS 2011. LNCS, vol.\u00a07078, pp. 34\u201349. Springer, Heidelberg (2011)"}],"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-642-35873-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T15:33:40Z","timestamp":1745940820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35873-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642358722","9783642358739"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35873-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}