{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:41:03Z","timestamp":1725536463112},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642032363"},{"type":"electronic","value":"9783642032370"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03237-0_9","type":"book-chapter","created":{"date-parts":[[2009,8,3]],"date-time":"2009-08-03T05:24:37Z","timestamp":1249277077000},"page":"102-119","source":"Crossref","is-referenced-by-count":2,"title":["Proving the Correctness of the Implementation of a Control-Command Algorithm"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Bouissou","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","first-page":"196","volume-title":"PLDI 2003","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: PLDI 2003, pp. 196\u2013207. ACM, New York (2003)"},{"key":"9_CR2","volume-title":"Follow-up of International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics","author":"O. Bouissou","year":"2007","unstructured":"Bouissou, O., Martel, M.: GRKLib: a guaranteed runge-kutta library. In: Follow-up of International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics. IEEE Press, Los Alamitos (2007)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-78163-9_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"O. Bouissou","year":"2008","unstructured":"Bouissou, O., Martel, M.: Abstract interpretation of the physical inputs of embedded programs. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-540-78739-6_5","volume-title":"Programming Languages and Systems","author":"O. Bouissou","year":"2008","unstructured":"Bouissou, O., Martel, M.: A hybrid denotational semantics of hybrid systems. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 63\u201377. Springer, Heidelberg (2008)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/3-540-63531-9_28","volume-title":"Software Engineering - ESEC-FSE \u201997","author":"Y. Chen","year":"1997","unstructured":"Chen, Y., Gansner, E., Koutsofios, E.: A C++ data model supporting reachability analysis and dead code detection. In: Jazayeri, M. (ed.) ESEC 1997 and ESEC-FSE 1997. LNCS, vol.\u00a01301, pp. 414\u2013431. Springer, Heidelberg (1997)"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/1190215.1190257","volume":"42","author":"B. Cook","year":"2007","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.: Proving that programs eventually do something good. SIGPLAN Notices\u00a042(1), 265\u2013276 (2007)","journal-title":"SIGPLAN Notices"},{"key":"9_CR7","first-page":"415","volume-title":"PLDI 2006","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, pp. 415\u2013426. ACM, New York (2006)"},{"key":"9_CR8","first-page":"238","volume-title":"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: POPL 1977, pp. 238\u2013252. ACM Press, New York (1977)"},{"issue":"4","key":"9_CR9","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"9_CR10","first-page":"224","volume-title":"SAFECOMPK 2002","author":"I.R. Oliveira de","year":"2002","unstructured":"de Oliveira, I.R., Cugnasca, P.S.: Checking safe trajectories of aircraft using hybrid automata. In: SAFECOMPK 2002, pp. 224\u2013235. Springer, Heidelberg (2002)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A. Fehnker","year":"2004","unstructured":"Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 326\u2013341. Springer, Heidelberg (2004)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C. Ferdinand","year":"2001","unstructured":"Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 469\u2013485. Springer, Heidelberg (2001)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: Phaver: Algorithmic verification of hybrid systems past hytech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"E. Goubault","year":"2006","unstructured":"Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 18\u201334. Springer, Heidelberg (2006)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","first-page":"215","volume-title":"Hybrid Systems: Computation and Control","author":"C. Guernic Le","year":"2008","unstructured":"Le Guernic, C., Girard, A.: Zonotope-hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 215\u2013228. Springer, Heidelberg (2008)"},{"key":"9_CR16","first-page":"147","volume-title":"POPL 2008","author":"A. Gupta","year":"2008","unstructured":"Gupta, A., Henzinger, T., Majumdar, R., Rybalchenko, A., Xu, R.: Proving non-termination. In: POPL 2008, pp. 147\u2013158. ACM Press, New York (2008)"},{"key":"9_CR17","first-page":"278","volume-title":"Symposium on Logic in Computer Science","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Symposium on Logic in Computer Science, pp. 278\u2013292. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/3-540-64358-3_40","volume-title":"Hybrid Systems: Computation and Control","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Rusu, V.: Reachability verification for hybrid automata. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.\u00a01386, pp. 190\u2013204. Springer, Heidelberg (1998)"},{"issue":"4","key":"9_CR19","first-page":"470","volume":"49","author":"J. Hespanha","year":"2004","unstructured":"Hespanha, J.: Uniform stability of switched linear systems: Extensions of LaSalle\u2019s invariance principle. IEEETAC\u00a049(4), 470\u2013482 (2004)","journal-title":"IEEETAC"},{"key":"9_CR20","unstructured":"Hymans, C., Levillain, O.: Newspeak, Doubleplussimple Minilang for Goodthinkful Static Analysis of C. Technical Note 2008-IW-SE-00010-1, EADS IW\/SE (2008)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-49163-5_9","volume-title":"Hybrid Systems V","author":"S. Kowalewski","year":"1999","unstructured":"Kowalewski, S., Stursberg, O., Fritz, M., Graf, H., Hoffmann, I., Preu\u00dfig, J., et al.: A case study in tool-aided analysis of discretely controlled continuous systems: the two tanks problem. In: Antsaklis, P.J., Kohn, W., Lemmon, M.D., Nerode, A., Sastry, S.S. (eds.) HS 1997. LNCS, vol.\u00a01567, p. 163. Springer, Heidelberg (1999)"},{"key":"9_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0017-8","volume-title":"Switching in Systems and Control","author":"D. Liberzon","year":"2003","unstructured":"Liberzon, D.: Switching in Systems and Control. Birkh\u00e4user, Boston (2003)"},{"key":"9_CR23","first-page":"377","volume-title":"Second IFAC Conference on Analysis and Design of Hybrid Systems","author":"I. Ben Makhlouf","year":"2006","unstructured":"Ben Makhlouf, I., Kowalewski, S.: An evaluation of two recent reachability analysis tools for hybrid systems. In: Second IFAC Conference on Analysis and Design of Hybrid Systems, pp. 377\u2013382. Elsevier, Amsterdam (2006)"},{"issue":"1","key":"9_CR24","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0096-3003(98)10083-8","volume":"105","author":"N.S. Nedialkov","year":"1999","unstructured":"Nedialkov, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Applied Mathematics and Computation\u00a0105(1), 21\u201368 (1999)","journal-title":"Applied Mathematics and Computation"},{"key":"9_CR25","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, E., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Dagstuhl Seminar 2003. LNCS, vol.\u00a02991, pp. 306\u2013313. Springer, Heidelberg (2004)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-540-78929-1_30","volume-title":"Hybrid Systems: Computation and Control","author":"N. Ramdani","year":"2008","unstructured":"Ramdani, N., Meslem, N., Candau, Y.: Reachability of uncertain nonlinear systems using a nonlinear hybridization. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 415\u2013428. Springer, Heidelberg (2008)"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11823230_2","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2006","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 3\u201317. Springer, Heidelberg (2006)"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/978-3-642-00602-9_28","volume-title":"HSCC 2009","author":"T. Wongpiromsarn","year":"2009","unstructured":"Wongpiromsarn, T., Mitra, S., Murray, R.M., Lamperski, A.G.: Periodically controlled hybrid systems. In: HSCC 2009. LNCS, vol.\u00a05469, pp. 396\u2013410. Springer, Heidelberg (2009)"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1007\/978-3-540-24743-2_42","volume-title":"Hybrid Systems: Computation and Control","author":"C. Yfoulis","year":"2004","unstructured":"Yfoulis, C., Shorten, R.: A numerical technique for stability analysis of linear switched systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 631\u2013645. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03237-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T07:46:27Z","timestamp":1552117587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03237-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032363","9783642032370"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03237-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}