{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:17:39Z","timestamp":1763468259546,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_20","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"308-324","source":"Crossref","is-referenced-by-count":23,"title":["Verifying the Safety of a Flight-Critical System"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Brat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Bushnell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Misty","family":"Davies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Falk","family":"Howar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Feret, J., Ghorbal, K., Goubault, E., Lesens, D., Mauborgne, L., Min\u00e9, A., Putot, S., Rival, X., Turin, M.: Space software validation using abstract interpretation. In: Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace, vol.\u00a0SP-669, pp. 1\u20137. ESA (2009)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"issue":"2-3","key":"20_CR3","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/B:FORM.0000040027.28662.a4","volume":"25","author":"G.P. Brat","year":"2004","unstructured":"Brat, G.P., Drusinsky, D., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M.R., Pasareanu, C.S., Venet, A., Visser, W., Washington, R.: Experimental evaluation of verification and validation tools on Martian rover software. Formal Methods in System Design\u00a025(2-3), 167\u2013198 (2004)","journal-title":"Formal Methods in System Design"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1987, pp. 178\u2013188. ACM (1987)","DOI":"10.1145\/41625.41641"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D. Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 126\u2013140. Springer, Heidelberg (2012)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Denney, E., Pai, G., Pohl, J.: AdvoCATE: An assurance case automation toolset. In: SAFECOMP Workshops, pp. 8\u201321 (2012)","DOI":"10.1007\/978-3-642-33675-1_2"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Dieumegard, A., Garoche, P.-L., Kahsai, T., Taillar, A., Thirioux, X.: Compilation of synchronous observers as code contracts. In: The 30th ACM\/SIGAPP Symposium on Applied Computing (2015)","DOI":"10.1145\/2695664.2695819"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Esteve, M., Katoen, J., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: 34th International Conference on Software Engineering, ICSE 2012, pp. 1022\u20131031 (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"20_CR9","unstructured":"Federal Aviation Administration. Electronic code of federal regulations"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-73445-1_13","volume-title":"Logic, Language, Information and Computation","author":"A.L. Galdino","year":"2007","unstructured":"Galdino, A.L., Mu\u00f1oz, C., Ayala-Rinc\u00f3n, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol.\u00a04576, pp. 177\u2013188. Springer, Heidelberg (2007)"},{"key":"20_CR11","unstructured":"Garavel, H., Graf, S.: Formal methods for safe and secure computer systems. Technical Report BSI-Study 875, Bundesamt fuer Sicherheit in Informationstechnik (December 2013)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-38088-4_10","volume-title":"NASA Formal Methods","author":"P.-L. Garoche","year":"2013","unstructured":"Garoche, P.-L., Kahsai, T., Tinelli, C.: Incremental invariant generation using logic-based automatic abstract transformers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 139\u2013154. Springer, Heidelberg (2013)"},{"issue":"1","key":"20_CR13","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10472-011-9224-3","volume":"63","author":"D. Giannakopoulou","year":"2011","unstructured":"Giannakopoulou, D., Bushnell, D.H., Schumann, J., Erzberger, H., Heere, K.: Formal testing for separation assurance. Ann. Math. Artif. Intell.\u00a063(1), 5\u201330 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Howar, F., Isberner, M., Lauderdale, T., Rakamaric, Z., Raman, V.: Taming test inputs for separation assurance. In: 19th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2014) (2014)","DOI":"10.1145\/2642937.2642940"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. In: Proceedings of the IEEE, pp. 1305\u20131320 (1991)","DOI":"10.1109\/5.97300"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: AMAST, pp. 83\u201396 (1993)","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K. Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 157\u2013171. Springer, Heidelberg (2012)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Howar, F., Giannakopoulou, D., Rakamaric, Z.: Hybrid learning: interface generation through static, dynamic, and symbolic analysis. In: International Symposium on Software Testing and Analysis, ISSTA, pp. 268\u2013279 (2013)","DOI":"10.1145\/2483760.2483783"},{"key":"20_CR19","unstructured":"Hueschen, R.M.: Development of the Transport Class Model (TCM) aircraft simulation from a sub-scale Generic Transport Model (GTM) simulation. Technical report, NASA, Langley Research Center, Hampton, VA (August 2011)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-642-20398-5_15","volume-title":"NASA Formal Methods","author":"T. Kahsai","year":"2011","unstructured":"Kahsai, T., Ge, Y., Tinelli, C.: Instantiation-based invariant discovery. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 192\u2013206. Springer, Heidelberg (2011)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKIND: a parallel k-induction based model checker. In: PDMC. EPTCS. EPTCS, vol.\u00a072, pp. 55\u201362 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"20_CR22","unstructured":"Lyapunov, A.: General problem of the stability of motion. PhD thesis, Univ. Kharkov (1892)"},{"issue":"2","key":"20_CR23","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"S.P. Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM\u00a053(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-05089-3_35","volume-title":"FM 2009: Formal Methods","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: A case study. In: Cavalcanti, A., Dams, D. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 547\u2013562. Springer, Heidelberg (2009)"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-33296-8_1","volume-title":"Formal Methods: Foundations and Applications","author":"J. Rushby","year":"2012","unstructured":"Rushby, J.: The versatile synchronous observer. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol.\u00a07498, pp. 1\u20131. Springer, Heidelberg (2012)"},{"key":"20_CR26","unstructured":"SmartCockpit. B737 automatic flight systems summary"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-75101-4_45","volume-title":"Computer Safety, Reliability, and Security","author":"J. Souyris","year":"2007","unstructured":"Souyris, J., Delmas, D.: Experimental assessment of Astr\u00e9e on safety-critical avionics software. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol.\u00a04680, pp. 479\u2013490. Springer, Heidelberg (2007)"},{"key":"20_CR28","unstructured":"Toom, A., Izerrouken, N., Naks, T., Pantel, M., Ssi-Yan-Kai, O.: Towards reliable code generation with an open tool: Evolutions of the Gene-Auto toolset. In: ERTS. Soci\u00e9t\u00e9 des Ing\u00e9nieurs de l\u2019Automobile (2010), \n                        http:\/\/www.sia.fr"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.\u00a08413, pp. 620\u2013635. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_54"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T09:03:43Z","timestamp":1676451823000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}