{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T19:14:29Z","timestamp":1725995669850},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030024499"},{"type":"electronic","value":"9783030024505"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-02450-5_16","type":"book-chapter","created":{"date-parts":[[2018,10,10]],"date-time":"2018-10-10T12:54:57Z","timestamp":1539176097000},"page":"270-283","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalization of Symplectic Geometry in HOL-Light"],"prefix":"10.1007","author":[{"given":"Guohui","family":"Wang","sequence":"first","affiliation":[]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[]},{"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Qianying","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Xiaojuan","family":"Li","sequence":"additional","affiliation":[]},{"given":"Yongdong","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,10,11]]},"reference":[{"issue":"4","key":"16_CR1","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1007\/s11075-017-0287-z","volume":"76","author":"M Anto\u00f1ana","year":"2017","unstructured":"Anto\u00f1ana, M., Makazaga, J., Murua, A.: Reducing and monitoring round-off error propagation for symplectic implicit Runge-Kutta schemes. Numer. Algorithms 76(4), 861\u2013880 (2017). https:\/\/doi.org\/10.1007\/s11075-017-0287-z . ISSN: 1572-9265","journal-title":"Numer. Algorithms"},{"issue":"07","key":"16_CR2","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1142\/S0218216506004798","volume":"15","author":"A Besana","year":"2006","unstructured":"Besana, A., Spera, M.: On some symplectic aspects of knot framings. J. Knot Theory Ramifications 15(07), 883\u2013912 (2006)","journal-title":"J. Knot Theory Ramifications"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12\u201327. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24364-6_2"},{"issue":"1-2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s00229-017-0934-7","volume":"155","author":"Giovanni Calvaruso","year":"2017","unstructured":"Calvaruso, G., Ovando, G.P.: From almost (para)-complex structures to affine structures on lie groups. Manuscripta Math. 155, 89\u2013113 (2016)","journal-title":"manuscripta mathematica"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"719","DOI":"10.4310\/JSG.2017.v15.n3.a4","volume":"15","author":"Pedro Frejlich","year":"2017","unstructured":"Frejlich, P., Torres, D.M., Miranda, E.: A note on the symplectic topology of b-manifolds. J. Symplectic Geom. 15, 719\u2013739 (2017)","journal-title":"Journal of Symplectic Geometry"},{"issue":"6","key":"16_CR6","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1007\/s00165-012-0232-9","volume":"25","author":"H Gottliebsen","year":"2013","unstructured":"Gottliebsen, H., Hardy, R., Lightfoot, O., Martin, U.: Applications of real number theorem proving in PVS. Formal Aspects Comput. 25(6), 993\u20131016 (2013)","journal-title":"Formal Aspects Comput."},{"issue":"12","key":"16_CR7","doi-asserted-by":"publisher","first-page":"3390","DOI":"10.1109\/TVLSI.2017.2751615","volume":"25","author":"XL Guo","year":"2017","unstructured":"Guo, X.L., Dutta, R.G., Mishra, P., Jin, Y.E.: Automatic code converter enhanced PCH framework for SoC trust verification. IEEE Trans. Very Large Scale Integr. Syst. 25(12), 3390\u20133400 (2017)","journal-title":"IEEE Trans. Very Large Scale Integr. Syst."},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"issue":"2104","key":"16_CR9","doi-asserted-by":"publisher","first-page":"20150399","DOI":"10.1098\/rsta.2015.0399","volume":"375","author":"JW Hunt","year":"2017","unstructured":"Hunt, J.W., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. Philos. Trans. 375(2104), 20150399 (2017)","journal-title":"Philos. Trans."},{"issue":"1","key":"16_CR10","first-page":"1","volume":"230","author":"JB Jeannin","year":"2015","unstructured":"Jeannin, J.B., et al.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. Int. J. Softw. Tools Technol. Transf. 230(1), 1\u201325 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"1409","DOI":"10.1090\/tran\/7188","volume":"370","author":"Yael Karshon","year":"2017","unstructured":"Karshon, Y., Ziltener, F.: Hamiltonian group actions on exact symplectic manifolds with proper momentum maps are standard. Trans. Am. Math. Soc. 370, 1409\u20131425 (2016)","journal-title":"Transactions of the American Mathematical Society"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Li, Y., Sun, M.: Modeling and verification of component connectors in Coq, vol. 113. Elsevier North-Holland, Inc. (2015)","DOI":"10.1016\/j.scico.2015.10.016"},{"issue":"4","key":"16_CR13","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1007\/s00006-016-0650-5","volume":"26","author":"S Ma","year":"2016","unstructured":"Ma, S., Shi, Z.P., Shao, Z.Z., Guan, Y., Li, L.M., Li, Y.D.: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm. Adv. Appl. Clifford Algebras 26(4), 1305\u20131330 (2016)","journal-title":"Adv. Appl. Clifford Algebras"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1016\/j.jcp.2017.03.018","volume":"338","author":"Lijie Mei","year":"2017","unstructured":"Mei, L.J., Wu, X.Y.: Symplectic exponential Runge Kutta methods for solving nonlinear Hamiltonian systems. J. Comput. Phys. 338, 567\u2013584 (2017)","journal-title":"Journal of Computational Physics"},{"issue":"1","key":"16_CR15","first-page":"63","volume":"152","author":"F Monteiro","year":"2017","unstructured":"Monteiro, F., Cordeiro, L., Filho, E.: ESBMC-GPU: a context-bounded model checking tool to verify CUDA programs. Sci. Comput. Program. 152(1), 63\u201369 (2017)","journal-title":"Sci. Comput. Program."},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"16_CR17","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1016\/j.amc.2017.11.054","volume":"323","author":"W Tang","year":"2018","unstructured":"Tang, W., Zhang, J.: Symplecticity-preserving continuous-stage Runge Kutta nystr$$\\ddot{o}$$m methods. Appl. Math. Comput. 323, 204\u2013219 (2018)","journal-title":"Appl. Math. Comput."},{"issue":"2","key":"16_CR18","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"16_CR19","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1016\/j.engfailanal.2017.04.004","volume":"82","author":"QX Wei","year":"2017","unstructured":"Wei, Q.X., Jiao, J., Zhao, T.D.: Flight control system failure modeling and verification based on spin. Eng. Fail. Anal. 82(1), 501\u2013513 (2017)","journal-title":"Eng. Fail. Anal."},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.isatra.2015.07.015","volume":"62","author":"CN Zhao","year":"2016","unstructured":"Zhao, C.N., Shi, L.K., Guan, Y., Li, X.J., Shi, Z.P.: Formal modeling and verification of fractional order linear systems. ISA Trans. 62, 87\u201393 (2016)","journal-title":"ISA Trans."},{"issue":"1","key":"16_CR21","first-page":"22","volume":"706","author":"CN Zhao","year":"2017","unstructured":"Zhao, C.N., Li, S.S.: Formalization of fractional order PD control systems in HOL4. Theoret. Comput. Sci. 706(1), 22\u201334 (2017)","journal-title":"Theoret. Comput. Sci."},{"key":"16_CR22","unstructured":"Zheng, X., Julien, C., Kim, M., Khurshid, S.: Perceptions on the state of the art in verification and validation in cyber-physical systems. IEEE Syst. J. PP(99), 1\u201314 (2015)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02450-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,3]],"date-time":"2022-09-03T19:01:21Z","timestamp":1662231681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02450-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030024499","9783030024505"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02450-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Gold Coast, QLD","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Australia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 November 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 November 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.formal-analysis.com\/icfem\/2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"22","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"14","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}