{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:40:36Z","timestamp":1743036036756,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031720437"},{"type":"electronic","value":"9783031720444"}],"license":[{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-72044-4_6","type":"book-chapter","created":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:02:41Z","timestamp":1725897761000},"page":"107-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Cyclone: A New Tool for\u00a0Verifying\/Testing Graph-Based Structures"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5010-4746","authenticated-orcid":false,"given":"Hao","family":"Wu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8075-2194","authenticated-orcid":false,"given":"Thomas","family":"Flinkow","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5231-6611","authenticated-orcid":false,"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,10]]},"reference":[{"key":"6_CR1","unstructured":"Lecomte, T., Servat, T., Pouzancre, G.: Formal methods in safety-critical railway systems. In: 10th Brasilian Symposium on Formal Methods (2007)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C Ferdinand","year":"2001","unstructured":"Ferdinand, C., et al.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469\u2013485. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45449-7_32"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In Sagiv, M. (ed.) Programming Languages and Systems, Springer, Berlin, pp. 21\u201330 (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Software Engineering and Formal Methods, SEFM 2012, LNCS, vol. 7504, pp. 233\u2013247. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6) 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","DOI":"10.1007\/s10009-010-0145-y"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods, CHARME 1999, LNCS, vol. 1703, pp. 54\u201366. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6","DOI":"10.1007\/3-540-48153-2_6"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. Electron. Proc. Theor. Comput. Sci. 310 50\u201362 (2019)","DOI":"10.4204\/EPTCS.310.6"},{"issue":"2","key":"6_CR8","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering, pp. 609\u2013619. IEEE (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"6_CR10","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages, pp. 53\u201364 (2011)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: International symposium of formal methods Europe, Springer, Cham, pp. 855\u2013874 (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Paulson, L.C. (ed.): : Zermelo-Fraenkel set theory. In: Isabelle. LNCS, vol. 828, pp. 203\u2013234. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030558","DOI":"10.1007\/BFb0030558"},{"key":"6_CR14","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer, Cham (2013)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (System description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Tim\u00a0Nelson, Ben\u00a0Greenman, S.P.: Forge: a tool and language for teaching formal methods. In: Object-Oriented Programming, Systems, Languages, and Application (2024)","DOI":"10.1145\/3649833"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.): Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-031-33163-3_13","volume-title":"Rigorous State-Based Methods","author":"H Wu","year":"2023","unstructured":"Wu, H., Cheng, Z.: Verifying event-b hybrid models using cyclone. In: Gl\u00e4sser, U., Creissac Campos, J., M\u00e9ry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 179\u2013184. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_13"},{"key":"6_CR19","unstructured":"Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company, Boston (1997)"},{"key":"6_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, USA (2004)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643\u2013644 (1974)","DOI":"10.1145\/361179.361202"},{"issue":"1","key":"6_CR22","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. Int. J. Softw. Tools Technol. Transfer 18(1), 67\u201391 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.scico.2014.04.015","volume":"94","author":"W Su","year":"2014","unstructured":"Su, W., Abrial, J.R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 94, 164\u2013202 (2014)","journal-title":"Sci. Comput. Program."},{"key":"6_CR24","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"9","key":"6_CR25","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019)","journal-title":"Commun. ACM"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"issue":"1","key":"6_CR27","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-28891-3_39","volume-title":"NASA Formal Methods","author":"P Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Miku\u010dionis, M., B\u00f8gsted Poulsen, D.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 449\u2013463. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_39"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Leuschel, M., Butler, M.: Prob: an automated analysis toolset for the b method. Int. J. Softw. Tools Technol. Transfer 10 185\u2013203 (2008). https:\/\/doi.org\/10.1007\/s10009-007-0063-9","DOI":"10.1007\/s10009-007-0063-9"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-030-85248-1_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Bendisposto","year":"2021","unstructured":"Bendisposto, J., et al.: ProB2-UI: a java-based user interface for ProB. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 193\u2013201. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_12"},{"issue":"4","key":"6_CR31","doi-asserted-by":"publisher","first-page":"1271","DOI":"10.1007\/s10270-020-00849-8","volume":"20","author":"H Wu","year":"2021","unstructured":"Wu, H., Farrell, M.: A formal approach to finding inconsistencies in a metamodel. Softw. Syst. Model. 20(4), 1271\u20131298 (2021). https:\/\/doi.org\/10.1007\/s10270-020-00849-8","journal-title":"Softw. Syst. Model."},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-030-99429-7_17","volume-title":"Fundamental Approaches to Software Engineering","author":"H Wu","year":"2022","unstructured":"Wu, H.: QMaxUSE: a query-based verification tool for UML class diagrams with OCL invariants. In: FASE 2022. LNCS, vol. 13241, pp. 310\u2013317. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_17"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-72044-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:05:26Z","timestamp":1725897926000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-72044-4_6"}},"subtitle":["Tool Paper"],"short-title":[],"issued":{"date-parts":[[2024,9,10]]},"ISBN":["9783031720437","9783031720444"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-72044-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,10]]},"assertion":[{"value":"10 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}