{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:48:49Z","timestamp":1742960929676,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030374860"},{"type":"electronic","value":"9783030374877"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-37487-7_11","type":"book-chapter","created":{"date-parts":[[2019,12,13]],"date-time":"2019-12-13T04:22:10Z","timestamp":1576210930000},"page":"125-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Metamodel-Based Approach for\u00a0Adding Modularization to\u00a0KeYmaera\u2019s Input Syntax"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8443-1558","authenticated-orcid":false,"given":"Thomas","family":"Baar","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,12,16]]},"reference":[{"key":"11_CR1","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"issue":"5","key":"11_CR2","doi-asserted-by":"publisher","first-page":"465","DOI":"10.18255\/1818-1015-2018-5-465-480","volume":"25","author":"T Baar","year":"2018","unstructured":"Baar, T., Staroletov, S.: A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier. Model. Anal. Inf. Syst. 25(5), 465\u2013480 (2018)","journal-title":"Model. Anal. Inf. Syst."},{"key":"11_CR3","volume-title":"Implementing Domain-Specific Languages with Xtext and Xtend","author":"L Bettini","year":"2016","unstructured":"Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend, 2nd edn. Packt Publisher, Birmingham (2016)","edition":"2"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Proceedings of Symposium on Applied Mathematics, pp. 19\u201332. Mathematical Aspects of Computer Science, American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"11_CR5","volume-title":"Metamodelling for Software Engineering","author":"C Gonzalez-Perez","year":"2008","unstructured":"Gonzalez-Perez, C., Henderson-Sellers, B.: Metamodelling for Software Engineering. Wiley, Hoboken (2008)"},{"key":"11_CR6","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic. Foundation of Computing","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundation of Computing. MIT Press, Cambridge (2000)"},{"key":"11_CR7","unstructured":"Harel, D., Meyer, A.R., Pratt, V.R.: Computability and completeness in logics of programs (preliminary report). In: Hopcroft, J.E., Friedman, E.P., Harrison, M.A. (eds.) Proceedings of the 9th Annual ACM Symposium on Theory of Computing, 4\u20136 May 1977, Boulder, Colorado, USA, pp. 261\u2013268. ACM (1977)"},{"issue":"10","key":"11_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-662-46681-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-B Jeannin","year":"2015","unstructured":"Jeannin, J.-B., et al.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21\u201336. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_2"},{"key":"11_CR10","volume-title":"Modeling and Analyzing Hybrid Systems with Sphinx - A User Manual","author":"S Mitsch","year":"2013","unstructured":"Mitsch, S.: Modeling and Analyzing Hybrid Systems with Sphinx - A User Manual. Carnegie Mellon University and Johannes Kepler University, Pittsburgh and Linz (2013). \nhttp:\/\/www.cs.cmu.edu\/afs\/cs\/Web\/People\/smitsch\/pdf\/userdoc.pdf"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: Newman, P., Fox, D., Hsu, D. (eds.) Robotics: Science and Systems IX, 24\u201328 June 2013. Technische Universit\u00e4t Berlin, Berlin (2013)","DOI":"10.15607\/RSS.2013.IX.014"},{"key":"11_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14509-4"},{"key":"11_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical Foundations of Cyber-Physical Systems","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Heidelberg (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"11_CR14","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.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547\u2013562. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-05089-3_35"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246\u2013265. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-10373-5_13"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: 17th Annual Symposium on Foundations of Computer Science, Houston, Texas, USA, 25\u201327 October 1976, pp. 109\u2013121. IEEE Computer Society (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-319-73579-5_10","volume-title":"Dynamic Logic. New Trends and Applications","author":"V Pratt","year":"2018","unstructured":"Pratt, V.: Dynamic logic: a personal perspective. In: Madeira, A., Benevides, M. (eds.) DALI 2017. LNCS, vol. 10669, pp. 153\u2013170. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73579-5_10"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"JD Quesel","year":"2016","unstructured":"Quesel, J.D., Mitsch, S., Loos, S., Ar\u00e9chiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. STTT 18(1), 67\u201391 (2016)","journal-title":"STTT"},{"key":"11_CR19","series-title":"Addison Wesley Object Technology Series","volume-title":"The Unified Modeling Language Reference Manuel - Covers UML 2.0","author":"JE Rumbaugh","year":"2005","unstructured":"Rumbaugh, J.E., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manuel - Covers UML 2.0. Addison Wesley Object Technology Series, 2nd edn. Addison-Wesley, Boston (2005)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-37487-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,15]],"date-time":"2019-12-15T19:04:03Z","timestamp":1576436643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-37487-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030374860","9783030374877"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-37487-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"16 December 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PSI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Andrei Ershov Memorial Conference on Perspectives of System Informatics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Novosibirsk","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Russia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ershov2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/psi.nsc.ru\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}