{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:13:45Z","timestamp":1767237225075,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642237010"},{"type":"electronic","value":"9783642237027"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23702-7_19","type":"book-chapter","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T17:31:31Z","timestamp":1315589491000},"page":"233-248","source":"Crossref","is-referenced-by-count":13,"title":["Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs"],"prefix":"10.1007","author":[{"given":"Peter","family":"Schrammel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Jeannet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","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":"19_CR2","first-page":"238","volume-title":"Principles of Programming Languages, POPL 1977","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: Principles of Programming Languages, POPL 1977, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"19_CR3","first-page":"84","volume-title":"Principles of Programming Languages, POPL 1978","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages, POPL 1978, pp. 84\u201397. ACM Press, New York (1978)"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design\u00a023, 5\u201337 (2003)","DOI":"10.1023\/A:1024480913162"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. Software Tools for Technology Transfer\u00a010, 401\u2013424 (2008)","DOI":"10.1007\/s10009-008-0064-3"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Schrammel, P., Jeannet, B.: Extending abstract acceleration to data-flow programs with numerical inputs. In: Numerical and Symbolic Abstract Domains, NSAD 2010. ENTCS, vol.\u00a0267, pp. 101\u2013114 (2010)","DOI":"10.1016\/j.entcs.2010.09.009"},{"key":"19_CR7","unstructured":"Jeannet, B.: Partitionnement Dynamique dans l\u2019Analyse de Relations Lin\u00e9aires et Application \u00e0 la V\u00e9rification de Programmes Synchrones. Th\u00e8se de doctorat, Grenoble INP (2000)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8_30","volume-title":"Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1990","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407. Springer, Heidelberg (1990)"},{"key":"19_CR10","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 iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol.\u00a0735, pp. 128\u2013141. Springer, Heidelberg (1993)"},{"key":"19_CR11","unstructured":"Gonnord, L.: Acc\u00e9l\u00e9ration abstraite pour l\u2019am\u00e9lioration de la pr\u00e9cision en Analyse des Relations Lin\u00e9aires. Th\u00e8se de doctorat, Universit\u00e9 Joseph Fourier, Grenoble (2007)"},{"key":"19_CR12","unstructured":"Gonnord, L.: The ASPIC tool: Accelerated symbolic polyhedral invariant computation (2009), http:\/\/laure.gonnord.org\/pro\/aspic\/aspic.html"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Schrammel, P., Jeannet, B.: Logico-numerical abstract acceleration and application to the verification of data-flow programs. Technical Report 7630, INRIA (2011)","DOI":"10.1007\/978-3-642-23702-7_19"},{"key":"19_CR14","unstructured":"Bres, Y., G\u00e9rard Berry, A.B., Sentovich, E.M.: State abstraction techniques for the verification of reactive circuits. In: Designing Correct Circuits, DCC 2002 (2002)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers\u00a035 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"19_CR16","unstructured":"Jeannet, B.: Bddapron: A logico-numerical abstract domain library (2009), http:\/\/pop-art.inrialpes.fr\/~bjeannet\/bjeannet-forge\/bddapron\/"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fernandez, J.C., Halbwachs, N.: Minimal model generation. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 197\u2013203. Springer, Heidelberg (1991)","DOI":"10.1007\/BFb0023733"},{"key":"19_CR18","volume-title":"Formal Methods in Computer-Aided Design, FMCAD 1908","author":"G. Hagen","year":"2008","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Formal Methods in Computer-Aided Design, FMCAD 2008. IEEE, Los Alamitos (2008)"},{"issue":"3","key":"19_CR19","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: Hysat: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design\u00a030, 179\u2013198 (2007)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23702-7_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T03:03:42Z","timestamp":1560567822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23702-7_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237010","9783642237027"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23702-7_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}