{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:06Z","timestamp":1740123366098,"version":"3.37.3"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,5,29]],"date-time":"2020-05-29T00:00:00Z","timestamp":1590710400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,29]],"date-time":"2020-05-29T00:00:00Z","timestamp":1590710400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100012338","name":"Alan Turing Institute","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012338","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools.<\/jats:p>","DOI":"10.1007\/s10817-020-09562-z","type":"journal-article","created":{"date-parts":[[2020,5,29]],"date-time":"2020-05-29T07:02:50Z","timestamp":1590735770000},"page":"157-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration"],"prefix":"10.1007","volume":"65","author":[{"given":"Dario","family":"Cattaruzza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,5,29]]},"reference":[{"key":"9562_CR1","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-78449-6_5","volume-title":"Control Subject to Computational and Communication Constraints: Current Challenges","author":"A Adimoolam","year":"2018","unstructured":"Adimoolam, A., Dang, T.: Template complex zonotope based stability verification. In: Tarbouriech, S., Girard, A., Hetel, L. (eds.) Control Subject to Computational and Communication Constraints: Current Challenges, pp. 83\u201396. Springer, Berlin (2018)"},{"key":"9562_CR2","unstructured":"Althoff, M.: An introduction to CORA 2015. In: ARCH@CPSWeek, EPiC Series in Computing, vol. 34, pp. 120\u2013151. EasyChair (2015)"},{"issue":"7","key":"9562_CR3","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"issue":"1","key":"9562_CR4","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF02293050","volume":"8","author":"D Avis","year":"1992","unstructured":"Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra. Discrete Comput. Geom. 8(1), 295\u2013313 (1992)","journal-title":"Discrete Comput. Geom."},{"key":"9562_CR5","first-page":"173","volume-title":"Hybrid Systems: Computation and Control","author":"S Bak","year":"2017","unstructured":"Bak, S., Duggirala, P.S.: HyLAA: a tool for computing simulation-equivalent reachability for linear systems. In: Alur, R. (ed.) Hybrid Systems: Computation and Control, pp. 173\u2013178. ACM, New York (2017)"},{"issue":"3","key":"9562_CR6","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1109\/37.506394","volume":"16","author":"S Bennett","year":"1996","unstructured":"Bennett, S.: A brief history of automatic control. IEEE Control Syst. 16(3), 17\u201325 (1996)","journal-title":"IEEE Control Syst."},{"issue":"4","key":"9562_CR7","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1002\/rnc.2914","volume":"24","author":"L Benvenuti","year":"2014","unstructured":"Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume-guarantee verification of nonlinear hybrid systems with Ariadne. Int. J. Robust Nonlinear Control 24(4), 699\u2013724 (2014)","journal-title":"Int. J. Robust Nonlinear Control"},{"key":"9562_CR8","first-page":"196","volume-title":"Programming Language Design and Implementation","author":"B 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: Plan, C. (ed.) Programming Language Design and Implementation, pp. 196\u2013207. ACM, New York (2003)"},{"key":"9562_CR9","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 589\u2013606. Springer, Berlin (2017)","DOI":"10.1007\/978-3-662-54577-5_34"},{"key":"9562_CR10","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-46430-1_10","volume-title":"Hybrid Systems: Computation and Control, LNCS","author":"O Botchkarev","year":"2000","unstructured":"Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Alur, R. (ed.) Hybrid Systems: Computation and Control, LNCS, pp. 73\u201388. Springer, Berlin (2000)"},{"key":"9562_CR11","unstructured":"Bouissou, O.: Analyse statique par interpr\u00e9tation abstraite de syst\u00e8mes hybrides. Ph.D. thesis, \u00c9cole Polytechnique (2008)"},{"key":"9562_CR12","doi-asserted-by":"crossref","unstructured":"Bouissou, O., Mimram, S., Chapoutot, A.: Hyson: set-based simulation of hybrid systems. In: Rapid System Prototyping (RSP), pp. 79\u201385. IEEE (2012)","DOI":"10.1109\/RSP.2012.6380694"},{"issue":"1","key":"9562_CR13","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF01449883","volume":"64","author":"C Carath\u00e9odory","year":"1907","unstructured":"Carath\u00e9odory, C.: \u00dcber den Variabilit\u00e4tsbereich der Koeffizienten von Potenzreihen, die gegebene Werte nicht annehmen. Math. Ann. 64(1), 95\u2013115 (1907)","journal-title":"Math. Ann."},{"key":"9562_CR14","doi-asserted-by":"crossref","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In: Static Analysis Symposium, LNCS, vol. 9291, pp. 312\u2013331. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-48288-9_18"},{"key":"9562_CR15","doi-asserted-by":"crossref","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration (extended version). Tech. rep., University of Oxford (2015). arXiv:1506.05607","DOI":"10.1007\/978-3-662-48288-9_18"},{"key":"9562_CR16","doi-asserted-by":"crossref","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Sound numerical computations in abstract acceleration. In: International Workshop on Numerical Software Verification, pp. 38\u201360. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-63501-9_4"},{"key":"9562_CR17","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Computer Aided Verification, LNCS, pp. 258\u2013263. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"9562_CR18","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: CDC, pp. 2089\u20132094. IEEE Computer Society (1998)","DOI":"10.1109\/CDC.1998.758642"},{"key":"9562_CR19","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: SMT-based verification of hybrid systems. In: AAAI Conference on Artificial Intelligence, p. 2100-2105. AAAI Press (2012)","DOI":"10.1609\/aaai.v26i1.8442"},{"key":"9562_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154\u2013169. Springer, Berlin (2000)","DOI":"10.1007\/10722167_15"},{"issue":"2","key":"9562_CR21","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/s10009-004-0182-5","volume":"7","author":"EM Clarke","year":"2005","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Computational challenges in bounded model checking. Int. J. Softw. Tools Technol. Transf. 7(2), 174\u2013183 (2005). https:\/\/doi.org\/10.1007\/s10009-004-0182-5","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9562_CR22","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Computer-Aided Verification, pp. 420\u2013432. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"9562_CR23","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)","DOI":"10.1145\/512950.512973"},{"key":"9562_CR24","doi-asserted-by":"crossref","unstructured":"Dang, T., Gawlitza, T.M.: Template-based unbounded time verification of affine hybrid automata. In: Asian Symposium on Programming Languages and Systems, LNCS, pp. 34\u201349. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25318-8_6"},{"key":"9562_CR25","doi-asserted-by":"crossref","unstructured":"Deng, Y., Rajhans, A., Julius, A.A.: STRONG: A trajectory-based verification toolbox for hybrid systems. In: Quantitative Evaluation of Systems, LNCS, vol. 8054, pp. 165\u2013168. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40196-1_13"},{"key":"9562_CR26","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: A verification tool for Stateflow models. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 68\u201382. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_5"},{"key":"9562_CR27","doi-asserted-by":"crossref","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT Modulo ODE: A direct SAT approach to hybrid systems. In: Automated Technology for Verification and Analysis, LNCS, vol. 5311, pp. 171\u2013185. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88387-6_14"},{"key":"9562_CR28","doi-asserted-by":"crossref","unstructured":"Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Hybrid Systems: Computation and Control, LNCS, pp. 326\u2013341. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24743-2_22"},{"issue":"3","key":"9562_CR29","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 Syst. Des. 30(3), 179\u2013198 (2007)","journal-title":"Formal Methods Syst. Des."},{"key":"9562_CR30","doi-asserted-by":"crossref","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Hybrid Systems: Computation and Control, LNCS, vol. 3414, pp. 258\u2013273. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"9562_CR31","doi-asserted-by":"crossref","unstructured":"Frehse, G., Le\u00a0Guernic, C., Donz\u00e9, A., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Computer-Aided Verification, LNCS, vol. 6806, pp. 379\u2013395. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"9562_CR32","doi-asserted-by":"crossref","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Combinatorics and computer science, pp. 91\u2013111. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61576-8_77"},{"key":"9562_CR33","doi-asserted-by":"crossref","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$-complete decision procedures for satisfiability over the reals. In: Automated Reasoning, pp. 286\u2013300. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"9562_CR34","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1006\/cviu.1998.0674","volume":"72","author":"PK Ghosh","year":"1998","unstructured":"Ghosh, P.K., Kumar, K.V.: Support function representation of convex bodies, its application in geometric computing, and some related representations. Comput. Vis. Image Underst. 72, 379\u2013403 (1998)","journal-title":"Comput. Vis. Image Underst."},{"key":"9562_CR35","doi-asserted-by":"crossref","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Hybrid Systems: Computation and Control, LNCS, vol. 3414, pp. 291\u2013305. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"9562_CR36","doi-asserted-by":"crossref","unstructured":"Girard, A., Le\u00a0Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hybrid Systems: Computation and Control, LNCS, vol. 3927, pp. 257\u2013271. Springer, Berlin (2006)","DOI":"10.1007\/11730637_21"},{"key":"9562_CR37","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Static Analysis Symposium, LNCS, pp. 144\u2013160. Springer, Berlin (2006)","DOI":"10.1007\/11823230_10"},{"issue":"Part B","key":"9562_CR38","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2013.09.016","volume":"93","author":"L Gonnord","year":"2014","unstructured":"Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Sci. Comput. Program. 93(Part B), 125\u2013153 (2014)","journal-title":"Sci. Comput. Program."},{"key":"9562_CR39","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Computer-Aided Verification, LNCS, vol. 5123, pp. 190\u2013203. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"9562_CR40","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Raymond, P., Proy, Y.E.: Verification of linear hybrid systems by means of convex approximations. In: Static Analysis Symposium, LNCS, vol. 864, pp. 223\u2013237. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58485-4_43"},{"issue":"1\u20132","key":"9562_CR41","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. J. Softw. Tools Technol. Transf. 1(1\u20132), 110\u2013122 (1997)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"9562_CR42","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139020411","volume-title":"Matrix Analysis","author":"RA Horn","year":"2012","unstructured":"Horn, R.A., Johnson, C.R.: Matrix Analysis. Cambridge University Press, Cambridge (2012)"},{"key":"9562_CR43","unstructured":"Jeannet, B.: Interproc analyzer for recursive programs with numerical variables (2010). http:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi"},{"key":"9562_CR44","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Principles of Programming Languages, pp. 529\u2013540. ACM, New York (2014)","DOI":"10.1145\/2578855.2535843"},{"key":"9562_CR45","unstructured":"Johnson, T.T., Mitra, S.: Passel: A verification tool for parameterized networks of hybrid automata (2012). https:\/\/publish.illinois.edu\/passel-tool\/"},{"issue":"4","key":"9562_CR46","doi-asserted-by":"publisher","first-page":"808","DOI":"10.1145\/6490.6496","volume":"33","author":"R Kannan","year":"1986","unstructured":"Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM (JACM) 33(4), 808\u2013821 (1986)","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"9562_CR47","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1109\/MCS.2006.1580151","volume":"26","author":"C Knospe","year":"2006","unstructured":"Knospe, C.: PID control. IEEE Control Syst. 26(1), 30\u201331 (2006)","journal-title":"IEEE Control Syst."},{"key":"9562_CR48","volume-title":"The Theory of Matrices","author":"P Lancaster","year":"1984","unstructured":"Lancaster, P., Tismenetsky, M.: The Theory of Matrices, 2nd edn. Academic Press, Cambridge (1984)","edition":"2"},{"key":"9562_CR49","doi-asserted-by":"crossref","unstructured":"Le\u00a0Guernic, C.: Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration. In: International Static Analysis Symposium, pp. 192\u2013211. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-66706-5_10"},{"key":"9562_CR50","doi-asserted-by":"crossref","unstructured":"Le\u00a0Guernic, C.: Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration (extended version) Working paper or preprint (2017). https:\/\/hal.inria.fr\/hal-01550767","DOI":"10.1007\/978-3-319-66706-5_10"},{"key":"9562_CR51","doi-asserted-by":"crossref","unstructured":"Le\u00a0Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: CAV, LNCS, vol. 5643, pp. 540\u2013554. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"9562_CR52","series-title":"Johns Hopkins Studies in Mathematical Sciences","volume-title":"Matrix Computations","author":"CF van Loan","year":"1996","unstructured":"van Loan, C.F., Golub, G.: Matrix Computations. Johns Hopkins Studies in Mathematical Sciences. JHU Press, Baltimore (1996)"},{"key":"9562_CR53","unstructured":"L\u00f6hner, R.: Einschlie\u00dfung der l\u00f6sung gew\u00f6hnlicher anfangs- und randwertaufgaben und anwendungen. Ph.D. thesis, Universit\u00e4t Karlsruhe (1988)"},{"key":"9562_CR54","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Proceedings of the twenty-fifth annual ACM-SIAM Symposium on Discrete Algorithms, pp. 366\u2013379. Society for Industrial and Applied Mathematics (2014)","DOI":"10.1137\/1.9781611973402.27"},{"key":"9562_CR55","doi-asserted-by":"crossref","unstructured":"Penrose, R.: A generalized inverse for matrices. In: Mathematical Proceedings of the Cambridge Philosophical Society, vol. 51\u20133, pp. 406\u2013413. Cambridge University Press, Cambridge (1955)","DOI":"10.1017\/S0305004100030401"},{"key":"9562_CR56","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Computer-Aided Verification, LNCS, vol. 6806, pp. 686\u2013702. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_56"},{"key":"9562_CR57","doi-asserted-by":"crossref","unstructured":"Schrammel, P.: Unbounded-time reachability analysis of hybrid systems by abstract acceleration. In: Embedded Software, pp. 51\u201354. IEEE (2015)","DOI":"10.1109\/EMSOFT.2015.7318259"},{"issue":"12","key":"9562_CR58","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. J. Symbol. Comput. 47(12), 1512\u20131532 (2012)","journal-title":"J. Symbol. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09562-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09562-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09562-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,6]],"date-time":"2024-08-06T16:48:59Z","timestamp":1722962939000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09562-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,29]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,2]]}},"alternative-id":["9562"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09562-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,5,29]]},"assertion":[{"value":"16 June 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}