{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T06:20:35Z","timestamp":1770358835331,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661063","type":"print"},{"value":"9783319661070","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_10","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"148-163","source":"Crossref","is-referenced-by-count":11,"title":["A Formal Proof in Coq of LaSalle\u2019s Invariance Principle"],"prefix":"10.1007","author":[{"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[]},{"given":"Damien","family":"Rouhling","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1080\/00207179.2013.826385","volume":"87","author":"I Barkana","year":"2014","unstructured":"Barkana, I.: Defending the beauty of the Invariance Principle. Int. J. Control 87(1), 186\u2013206 (2014). http:\/\/dx.doi.org\/10.1080\/00207179.2013.826385","journal-title":"Int. J. Control"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2","volume-title":"Interactive Theorem Proving","year":"2013","unstructured":"Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): ITP 2013. LNCS, vol. 7998. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015). http:\/\/dx.doi.org\/10.1007\/s11786-014-0181-1","journal-title":"Math. Comput. Sci."},{"key":"10_CR4","unstructured":"Cano, G.: Interaction entre alg\u00e8bre lin\u00e9aire et analyse en formalisation des math\u00e9matiques. (Interaction between linear algebra and analysis in formal mathematics). Ph.D. thesis, University of Nice Sophia Antipolis, France (2014). https:\/\/tel.archives-ouvertes.fr\/tel-00986283"},{"key":"10_CR5","unstructured":"Chan, M., Ricketts, D., Lerner, S., Malecha, G.: Formal Verification of Stability Properties of Cyber-Physical Systems, January 2016"},{"issue":"4\u20135","key":"10_CR6","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/S0167-6911(99)00076-6","volume":"38","author":"V Chellaboina","year":"1999","unstructured":"Chellaboina, V., Leonessa, A., Haddad, W.M.: Generalized Lyapunov and invariant set theorems for nonlinear dynamical systems. Syst. Control Lett. 38(4\u20135), 289\u2013295 (1999). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167691199000766","journal-title":"Syst. Control Lett."},{"issue":"2","key":"10_CR7","first-page":"383","volume":"1","author":"A Darmochwa\u0142","year":"1990","unstructured":"Darmochwa\u0142, A.: Compact Spaces. Formaliz. Math. 1(2), 383\u2013386 (1990). http:\/\/fm.mizar.org\/1990-1\/pdf1-2\/compts_1.pdf","journal-title":"Formaliz. Math."},{"issue":"9","key":"10_CR8","doi-asserted-by":"publisher","first-page":"2333","DOI":"10.1109\/TAC.2013.2246900","volume":"58","author":"NR Fischer","year":"2013","unstructured":"Fischer, N.R., Kamalapurkar, R., Dixon, W.E.: LaSalle-Yoshizawa Corollaries for Nonsmooth Systems. IEEE Trans. Automat. Control 58(9), 2333\u20132338 (2013). http:\/\/dx.doi.org\/10.1109\/TAC.2013.2246900","journal-title":"IEEE Trans. Automat. Control"},{"issue":"11","key":"10_CR9","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal Proof - The Four-Color Theorem. Notices AMS 55(11), 1382\u20131393 (2008)","journal-title":"Notices AMS"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Gonthier, G., et al.: A Machine-Checked Proof of the Odd Order Theorem. In: Blazy et al. [2], pp. 163\u2013179 (2013). doi:10.1007\/978-3-642-39634-2_14","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"10_CR11","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2015). https:\/\/hal.inria.fr\/inria-00258384"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-28891-3_15","volume-title":"NASA Formal Methods","author":"H Herencia-Zapana","year":"2012","unstructured":"Herencia-Zapana, H., Jobredeaux, R., Owre, S., Garoche, P.-L., Feron, E., Perez, G., Ascariz, P.: PVS linear algebra libraries for verification of control software algorithms in C\/ACSL. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 147\u2013161. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28891-3_15"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type Classes and Filters for Mathematical Analysis in Isabelle\/HOL. In: Blazy et al. [2], pp. 279\u2013294 (2013). doi:10.1007\/978-3-642-39634-2_21","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"10_CR14","unstructured":"Khalil, H.: Nonlinear Systems. Pearson Education, Prentice Hall (2002). https:\/\/books.google.fr\/books?id=t_d1QgAACAAJ"},{"issue":"4","key":"10_CR15","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1109\/TCT.1960.1086720","volume":"7","author":"J LaSalle","year":"1960","unstructured":"LaSalle, J.: Some Extensions of Liapunov\u2019s Second Method. IRE Trans. Circ. Theory 7(4), 520\u2013527 (1960)","journal-title":"IRE Trans. Circ. Theory"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Lester, D.R.: Topology in PVS: Continuous Mathematics with Applications. In: Proceedings of the Second Workshop on Automated Formal Methods, AFM 2007, pp. 11\u201320. ACM, New York (2007). http:\/\/doi.acm.org\/10.1145\/1345169.1345171","DOI":"10.1145\/1345169.1345171"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Liapounoff, A.: Probl\u00e8me g\u00e9n\u00e9ral de la stabilit\u00e9 du mouvement. In: Annales de la Facult\u00e9 des sciences de Toulouse: Math\u00e9matiques, vol. 9, pp. 203\u2013474 (1907). http:\/\/eudml.org\/doc\/72801","DOI":"10.5802\/afst.246"},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0167-6911(00)00025-6","volume":"40","author":"R Lozano","year":"2000","unstructured":"Lozano, R., Fantoni, I., Block, D.: Stabilization of the inverted pendulum around its homoclinic orbit. Syst. Control Lett. 40(3), 197\u2013204 (2000)","journal-title":"Syst. Control Lett."},{"issue":"5","key":"10_CR19","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.sysconle.2005.07.009","volume":"55","author":"JL Mancilla-Aguilar","year":"2006","unstructured":"Mancilla-Aguilar, J.L., Garc\u00eda, R.A.: An extension of LaSalle\u2019s invariance principle for switched systems. Syst. Control Lett. 55(5), 376\u2013384 (2006). http:\/\/dx.doi.org\/10.1016\/j.sysconle.2005.07.009","journal-title":"Syst. Control Lett."},{"key":"10_CR20","unstructured":"Mayero, M.: Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique. Ph.D. thesis, Universit\u00e9 Paris VI (d\u00e9cembre 2001)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-71067-7_20","volume-title":"Theorem Proving in Higher Order Logics","author":"S Mitra","year":"2008","unstructured":"Mitra, S., Chandy, K.M.: A Formalized Theory for Verifying Stability and Convergence of Automata in PVS. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 230\u2013245. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-71067-7_20"},{"issue":"1","key":"10_CR22","first-page":"223","volume":"1","author":"B Padlewska","year":"1990","unstructured":"Padlewska, B., Darmochwa\u0142, A.: Topological Spaces and Continuous Functions. Formaliz. Math. 1(1), 223\u2013230 (1990). http:\/\/fm.mizar.org\/1990-1\/pdf1-1\/pre_topc.pdf","journal-title":"Formaliz. Math."},{"key":"10_CR23","unstructured":"The Coq Development Team: The Coq proof assistant reference manual, version 8.6. (2016). http:\/\/coq.inria.fr"},{"key":"10_CR24","unstructured":"Wilansky, A.: Topology for Analysis. Dover Books on Mathematics. Dover Publications, New York (2008). http:\/\/cds.cern.ch\/record\/2222525"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:05:39Z","timestamp":1664431539000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}