{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:52Z","timestamp":1763468152309},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410093"},{"type":"electronic","value":"9783642410109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41010-9_1","type":"book-chapter","created":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T09:31:39Z","timestamp":1379323899000},"page":"1-16","source":"Crossref","is-referenced-by-count":3,"title":["Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-linear and Linear Analyses"],"prefix":"10.1007","author":[{"given":"Adrien","family":"Champion","sequence":"first","affiliation":[]},{"given":"R\u00e9mi","family":"Delmas","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Dierkes","sequence":"additional","affiliation":[]},{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[]},{"given":"Romain","family":"Jobredeaux","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Roux","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","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":"1_CR2","unstructured":"Champion, A., Delmas, R.: Stuff: Stuff is the ultimate formal framework., https:\/\/cavale.enseeiht.fr\/redmine\/projects\/stuff"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Champion, A., Delmas, R., Dierkes, M.: Generating property-directed potential invariants by backward analysis. In: FTSCS, pp. 22\u201338 (2012)","DOI":"10.4204\/EPTCS.105.3"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"1_CR5","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: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201397. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-24431-5_9","volume-title":"Formal Methods for Industrial Critical Systems","author":"M. Dierkes","year":"2011","unstructured":"Dierkes, M.: Formal analysis of a triplex sensor voter in an industrial context. In: Sala\u00fcn, G., Sch\u00e4tz, B. (eds.) FMICS 2011. LNCS, vol.\u00a06959, pp. 102\u2013116. Springer, Heidelberg (2011)"},{"key":"1_CR8","unstructured":"Feron, E., Brat, G.: Formal methods for areospace applications. In: FMCAD 2012 Tutorial (2012)"},{"key":"1_CR9","unstructured":"Garoche, P.-L., Roux, P.: SMT-AI: SMT abstract interpreter, https:\/\/cavale.enseeiht.fr\/redmine\/projects\/smt-ai"},{"key":"1_CR10","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":"1_CR11","doi-asserted-by":"crossref","unstructured":"Gawlitza, T., Seidl, H., Adj\u00e9, A., Gaubert, S., Goubault, E.: Abstract interpretation meets convex optimization. J. Symb. Comput.\u00a047(12) (2012)","DOI":"10.1016\/j.jsc.2011.12.048"},{"key":"1_CR12","unstructured":"K\u00e4stner, D., Wilhelm, S., Nenova, S., Cousot, P., Cousot, R., Feret, J., Min\u00e9, A., Mauborgne, L., Rival, X.: Astr\u00e9e: Proving the absence of runtime errors. In: ERTSS (2010)"},{"key":"1_CR13","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)"},{"key":"1_CR14","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: AST (satt. of WCRE), pp. 310\u2013319. IEEE (2001)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 585\u2013599. Springer, Heidelberg (2010)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Roux, P., Jobredeaux, R., Garoche, P.L., F\u00e9ron, E.: A generic ellipsoid abstract domain for linear time invariant systems. In: HSCC. ACM (2012)","DOI":"10.1145\/2185632.2185651"},{"key":"1_CR17","unstructured":"Rowell, D.: Dicrete time observers and lqg control. MIT, Dpt. of Mechanical Engineering \u2013 2.151 Advanced System Dynamics and Control (2004), http:\/\/web.mit.edu\/2.151\/www\/Handouts\/Kalman.pdf"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Souyris, J., Favre-Flix, D.: Proof of properties in avionics. In: Building the Information Society, vol.\u00a0156, pp. 527\u2013535. Springer (2004)","DOI":"10.1007\/978-1-4020-8157-6_48"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry: Prepared for publication with the assistance of j.c.c. mckinsey. Technical report, RAND Corporation (1951)","DOI":"10.1525\/9780520348097"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Tinelli, C.: Foundations of satisfiability modulo theories. In: WoLLIC, p. 58 (2010)","DOI":"10.1007\/978-3-642-13824-9_6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41010-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,6]],"date-time":"2022-03-06T07:04:13Z","timestamp":1646550253000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41010-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410093","9783642410109"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41010-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}