{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T04:24:12Z","timestamp":1774671852904,"version":"3.50.1"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T00:00:00Z","timestamp":1669766400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T00:00:00Z","timestamp":1669766400000},"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":["Softw Syst Model"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1007\/s10270-022-01063-4","type":"journal-article","created":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T07:07:55Z","timestamp":1669792075000},"page":"1473-1494","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["The ForeMoSt approach to building valid model-based safety arguments"],"prefix":"10.1007","volume":"22","author":[{"given":"Torin","family":"Viger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Logan","family":"Murphy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessio","family":"Di Sandro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramy","family":"Shahin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,30]]},"reference":[{"key":"1063_CR1","unstructured":"ISO: ISO26262: Road Vehicles\u2014Functional Safety. ISO, Geneva (2011)"},{"key":"1063_CR2","unstructured":"SOTIF: ISO\/PAS 21448:2019: Road Vehicles\u2014Safety of the Intended Functionality. ISO (2019)"},{"key":"1063_CR3","unstructured":"Kelly, T.P.: Arguing safety: a systematic approach to managing safety cases. Ph.D. thesis, University of York, UK (1999)"},{"issue":"7","key":"1063_CR4","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1016\/j.infsof.2014.03.001","volume":"56","author":"S Nair","year":"2014","unstructured":"Nair, S., De La Vara, J.L., Sabetzadeh, M., Briand, L.: An extended systematic literature review on provision of evidence for safety certification. Inf. Softw. Technol. 56(7), 689\u2013717 (2014)","journal-title":"Inf. Softw. Technol."},{"key":"1063_CR5","unstructured":"Goal Structuring Notation Community Standard (Version 2). Jan (2018)"},{"key":"1063_CR6","doi-asserted-by":"crossref","unstructured":"Barry, M.R.: CertWare: a workbench for safety case production and analysis. In: Proceedings of 2011 Aerospace Conference, pp. 1\u201310. IEEE (2011)","DOI":"10.1109\/AERO.2011.5747648"},{"key":"1063_CR7","doi-asserted-by":"crossref","unstructured":"Di Sandro, A., Selim, G.M.K., Salay, R., Viger, T., Chechik, M., Kokaly, S.: MMINT-A 2.0: tool support for the lifecycle of model-based safety artifacts. In: Proceedings of MODELS\u201920 Companion, pp. 15\u20131155. ACM (2020)","DOI":"10.1145\/3417990.3422012"},{"key":"1063_CR8","unstructured":"Astah. https:\/\/astah.net\/products\/astah-gsn\/ (2021)"},{"key":"1063_CR9","unstructured":"Ansys Medini Analyze. https:\/\/www.ansys.com\/products\/safety-analysis\/ansys-medini-analyze (2021)"},{"key":"1063_CR10","unstructured":"IBM Rhapsody. https:\/\/www.ibm.com\/docs\/en\/rhapsody (2021)"},{"key":"1063_CR11","unstructured":"Greenwell, W.S., Knight, J.C., Holloway, C.M., Pease, J.J.: A taxonomy of fallacies in system safety arguments. In: Proceedings of ISSC\u201906 (2006)"},{"key":"1063_CR12","unstructured":"Haddon-Cave, C.: The nimrod review: an independent review into the broader issues surrounding the loss of the RAF nimrod MR2 aircraft XV230 (2009)"},{"key":"1063_CR13","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"1063_CR14","doi-asserted-by":"crossref","unstructured":"Viger, T., Salay, R., Selim, G., Chechik, M.: Just enough formality in assurance argument structures. In: Proceedings of SAFECOMP\u201920, pp. 34\u201349. Springer (2020)","DOI":"10.1007\/978-3-030-54549-9_3"},{"key":"1063_CR15","doi-asserted-by":"crossref","unstructured":"Viger, T., Murphy, L., Di Sandro, A., Shahin, R., Chechik, M.: A lean approach to building valid model-based safety arguments. In: Proceedings of MODELS\u201921, pp. 194\u2013204. IEEE (2021)","DOI":"10.1007\/s10270-022-01063-4"},{"key":"1063_CR16","doi-asserted-by":"crossref","unstructured":"Murphy, L., Viger, T., Di Sandro, A., Shahin, R., Chechik, M.: Validating safety arguments with lean. In: Proceedings of SEFM\u201921. LNCS, vol. 13085, pp. 23\u201343. Springer (2021)","DOI":"10.1007\/978-3-030-92124-8_2"},{"key":"1063_CR17","doi-asserted-by":"crossref","unstructured":"de Moura, L., Kong, S., Avigad, J., Van\u00a0Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Proceedings of CADE\u201915, pp. 378\u2013388 (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"1063_CR18","volume-title":"State Models and Java Programs","author":"J Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: State Models and Java Programs. Wiley, Hoboken (1999)"},{"key":"1063_CR19","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: Proceedings of ASE\u201908, pp. 475\u2013476. IEEE (2008)","DOI":"10.1109\/ASE.2008.78"},{"issue":"3","key":"1063_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10515-005-2641-y","volume":"12","author":"D Giannakopoulou","year":"2005","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. J. Autom. Softw. Eng. 12(3), 297\u2013320 (2005)","journal-title":"J. Autom. Softw. Eng."},{"key":"1063_CR21","doi-asserted-by":"crossref","unstructured":"Sljivo, I., Gallina, B., Carlson, J., Hansson, H., Puri, S.: Tool-supported safety-relevant component reuse: from specification to argumentation. In: Ada-Europe International Conference on Reliable Software Technologies, pp. 19\u201333. Springer (2018)","DOI":"10.1007\/978-3-319-92432-8_2"},{"key":"1063_CR22","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1016\/j.jss.2016.07.034","volume":"131","author":"I Sljivo","year":"2017","unstructured":"Sljivo, I., Gallina, B., Carlson, J., Hansson, H., Puri, S.: A method to generate reusable safety case argument-fragments from compositional safety analysis. J. Syst. Softw. 131, 570\u2013590 (2017)","journal-title":"J. Syst. Softw."},{"key":"1063_CR23","doi-asserted-by":"crossref","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Proceedings of ICCL\u201988, pp. 50\u201366. Springer (1988)","DOI":"10.1007\/3-540-52335-9_47"},{"key":"1063_CR24","doi-asserted-by":"crossref","unstructured":"Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of ICFP\u201917, pp. 1\u201329. ACM (2017)","DOI":"10.1145\/3110278"},{"key":"1063_CR25","unstructured":"GSN Working Group: GSN community standard version 2. http:\/\/www.goalstructuringnotation.info\/. York, UK (2011)"},{"issue":"3","key":"1063_CR26","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/s10515-017-0230-5","volume":"25","author":"E Denney","year":"2018","unstructured":"Denney, E., Pai, G.: Tool support for assurance case development. J. Autom. Softw. Eng. 25(3), 435\u2013499 (2018)","journal-title":"J. Autom. Softw. Eng."},{"key":"1063_CR27","volume-title":"EMF: Eclipse Modeling Framework","author":"D Steinberg","year":"2008","unstructured":"Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education, London (2008)"},{"key":"1063_CR28","unstructured":"B\u00e9zivin, J., Jouault, F., Valduriez, P.: On the need for megamodels. In: OOPSLA\/GPCE Workshops\u201904 (2004)"},{"issue":"1","key":"1063_CR29","first-page":"231","volume":"19","author":"R Salay","year":"2020","unstructured":"Salay, R., Kokaly, S., Di Sandro, A., Fung, N.L.S., Chechik, M.: Heterogeneous megamodel management using collection operators. SoSyM 19(1), 231\u2013260 (2020)","journal-title":"SoSyM"},{"key":"1063_CR30","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Property specification patterns for finite-state verification. In: Proceedings of Workshop on Formal Methods in Software Practice (1998)","DOI":"10.1145\/298595.298598"},{"key":"1063_CR31","doi-asserted-by":"crossref","unstructured":"Di Sandro, A., Kokaly, S., Salay, R., Chechik, M.: Querying automotive system models and safety artifacts with MMINT and Viatra. In: Proceedings of MODELS\u201919 Companion, pp. 2\u201311. IEEE (2019)","DOI":"10.1109\/MODELS-C.2019.00008"},{"key":"1063_CR32","doi-asserted-by":"publisher","first-page":"34","DOI":"10.2991\/jase.d.200912.001","volume":"1","author":"A Di Sandro","year":"2020","unstructured":"Di Sandro, A., Kokaly, S., Salay, R., Chechik, M.: Querying automotive system models and safety artifacts: tool support and case study. J. Automot. Softw. Eng. 1, 34\u201350 (2020)","journal-title":"J. Automot. Softw. Eng."},{"issue":"3","key":"1063_CR33","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/s10270-016-0530-4","volume":"15","author":"D Varr\u00f3","year":"2016","unstructured":"Varr\u00f3, D., Bergmann, G., Heged\u00fcs, \u00c1., Horv\u00e1th, \u00c1., R\u00e1th, I., Ujhelyi, Z.: Road to a Reactive and incremental model transformation platform: three generations of the VIATRA framework. Softw. Syst. Model. 15(3), 609\u2013629 (2016)","journal-title":"Softw. Syst. Model."},{"key":"1063_CR34","doi-asserted-by":"crossref","unstructured":"The Mathlib Community: The lean mathematical library. In: Proceedings of CPP\u201920. ACM (2020)","DOI":"10.1145\/3372885.3373824"},{"key":"1063_CR35","doi-asserted-by":"crossref","unstructured":"Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P.L., Zhang, Y., Jetley, R.P.: Safety-assured development of the GPCA infusion pump software. In: Proceedings of EMSOFT\u201911, pp. 155\u2013164. ACM (2011)","DOI":"10.1145\/2038642.2038667"},{"key":"1063_CR36","doi-asserted-by":"publisher","unstructured":"Viger, T., Murphy, L., Di\u00a0Sandro, A., Menghi, C., Shahin, R., Chechik, M.: The ForeMoSt approach to building valid model-based safety arguments. https:\/\/doi.org\/10.5281\/zenodo.6360845","DOI":"10.5281\/zenodo.6360845"},{"key":"1063_CR37","doi-asserted-by":"crossref","unstructured":"Ayoub, A., Kim, B., Lee, I., Sokolsky, O.: A safety case pattern for model-based development approach. In: Lecture Notes in Computer Science, vol. 7226, pp. 141\u2013146. Springer (2012)","DOI":"10.1007\/978-3-642-28891-3_14"},{"key":"1063_CR38","unstructured":"Rushby, J., Xu, X., Rangarajan, M., Weaver, T.L.: Understanding and evaluating assurance cases. NASA Contractor Report NASA\/CR-2015-218802, NASA Langley Research Center (2015)"},{"key":"1063_CR39","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1063_CR40","unstructured":"Arney, D.E., Jetley, R., Jones, P., Lee, I., Ray, A., Sokolsky, O., Zhang, Y.: Generic infusion pump hazard analysis and safety requirements version 1.0. Technical report, CIS (2009)"},{"issue":"2","key":"1063_CR41","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163\u2013203 (2011)","journal-title":"Comput. Sci. Rev."},{"issue":"3","key":"1063_CR42","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3166\/ejc.18.217-238","volume":"18","author":"A Sangiovanni-Vincentelli","year":"2012","unstructured":"Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217\u2013238 (2012)","journal-title":"Eur. J. Control"},{"key":"1063_CR43","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2377656.2377659","volume":"21","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Validation of requirements for hybrid systems: a formal approach. ACM Trans. Softw. Eng. Methodol. 21, 1\u201334 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1063_CR44","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: Proceedings of ASE\u201913, pp. 702\u2013705. IEEE Press (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"1063_CR45","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program."},{"key":"1063_CR46","doi-asserted-by":"crossref","unstructured":"G\u00e9rard, S., Dumoulin, C., Tessier, P., Selic, B.: Papyrus: a UML2 tool for domain-specific language modeling model-based engineering of embedded real-time systems, pp. 361\u2013368 (2011)","DOI":"10.1007\/978-3-642-16277-0_19"},{"key":"1063_CR47","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: Proceedings 38th Euromicro Conference on Software Engineering and Advanced Applications, pp. 21\u201328. IEEE (2012)","DOI":"10.1109\/SEAA.2012.68"},{"key":"1063_CR48","doi-asserted-by":"crossref","unstructured":"Pakonen, A., Pang, C., Buzhinsky, I., Vyatkin, V.: User-friendly formal specification languages-conclusions drawn from industrial experience on model checking. In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA), pp. 1\u20138. IEEE (2016)","DOI":"10.1109\/ETFA.2016.7733717"},{"key":"1063_CR49","doi-asserted-by":"crossref","unstructured":"Filipovikj, P., Jagerfield, T., Nyberg, M., Rodriguez-Navas, G., Seceleanu, C.: Integrating pattern-based formal requirements specification in an industrial tool-chain. In: 2016 IEEE 40th Annual Computer Software and Applications Conference (COMPSAC), vol. 2, pp. 167\u2013173. IEEE (2016)","DOI":"10.1109\/COMPSAC.2016.140"},{"key":"1063_CR50","doi-asserted-by":"crossref","unstructured":"Cobleigh, R.L., Avrunin, G.S., Clarke, L.A.: User guidance for creating precise and accessible property specifications. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 208\u2013218 (2006)","DOI":"10.1145\/1181775.1181801"},{"key":"1063_CR51","doi-asserted-by":"crossref","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Proceedings of VMCAI\u201913. LNCS, vol. 7737, pp. 275\u2013294. Springer (2013)","DOI":"10.1007\/978-3-642-35873-9_18"},{"key":"1063_CR52","doi-asserted-by":"crossref","unstructured":"Diskin, Z., Maibaum, T., Wassyng, A., Wynn-Williams, S., Lawford, M.: Assurance via model transformations and their hierarchical refinement. In: Proceedings of MODELS\u201918, pp. 426\u2013436 (2018)","DOI":"10.1145\/3239372.3239413"},{"key":"1063_CR53","doi-asserted-by":"crossref","unstructured":"Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T.: Isabelle\/SACM: computer-assisted assurance cases with integrated formal methods. In: Proceedings of iFM\u201919, pp. 379\u2013398. Springer (2019)","DOI":"10.1007\/978-3-030-34968-4_21"},{"issue":"4","key":"1063_CR54","doi-asserted-by":"publisher","first-page":"830","DOI":"10.1109\/TR.2014.2335995","volume":"63","author":"E Denney","year":"2014","unstructured":"Denney, E., Pai, G.: Automating the assembly of aviation safety cases. IEEE Trans. Reliab. 63(4), 830\u2013849 (2014)","journal-title":"IEEE Trans. Reliab."},{"key":"1063_CR55","doi-asserted-by":"crossref","unstructured":"Kelly, T., McDermid, J.: Safety case construction and reuse using patterns. In: Proceedings of SAFECOMP\u201997, pp. 55\u201369. Springer (1997)","DOI":"10.1007\/978-1-4471-0997-6_5"},{"key":"1063_CR56","unstructured":"Picardi, C., Paterson, C., Hawkins, R.D., Calinescu, R., Habli, I.: Assurance argument patterns and processes for machine learning in safety-related systems. In: Proceedings of the Workshop on Artificial Intelligence Safety (SafeAI 2020), pp. 23\u201330. CEUR Workshop Proceedings (2020)"},{"key":"1063_CR57","doi-asserted-by":"crossref","unstructured":"Gleirscher, M., Carlan, C.: Arguing from hazard analysis in safety cases: a modular argument pattern. In: 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), pp. 53\u201360. IEEE (2017)","DOI":"10.1109\/HASE.2017.15"},{"key":"1063_CR58","doi-asserted-by":"crossref","unstructured":"Chowdhury, T., Lin, C.-W., Kim, B., Lawford, M., Shiraishi, S., Wassyng, A.: Principles for systematic development of an assurance case template from ISO 26262. In: International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 69\u201372. IEEE (2017)","DOI":"10.1109\/ISSREW.2017.14"},{"key":"1063_CR59","doi-asserted-by":"crossref","unstructured":"Hawkins, R., Kelly, T., Knight, J., Graydon, P.: A new approach to creating clear safety arguments. In: Advances in Systems Safety, pp. 3\u201323. Springer (2011)","DOI":"10.1007\/978-0-85729-133-2_1"},{"key":"1063_CR60","doi-asserted-by":"crossref","unstructured":"Chowdhury, T., Wassyng, A., Paige, R.F., Lawford, M.: Systematic evaluation of (safety) assurance cases. In: International Conference on Computer Safety, Reliability, and Security, pp. 18\u201333. Springer (2020)","DOI":"10.1007\/978-3-030-54549-9_2"},{"issue":"4","key":"1063_CR61","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"1063_CR62","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Proceedings of SOSP\u201909, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"1063_CR63","doi-asserted-by":"crossref","unstructured":"Shahin, R., Kokaly, S., Chechik, M.: Towards certified analysis of software product line safety cases. In: Proceedings of SAFECOMP\u201921. LNCS, vol. 12852, pp. 130\u2013145. Springer (2021)","DOI":"10.1007\/978-3-030-83903-1_9"},{"key":"1063_CR64","doi-asserted-by":"crossref","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603022"},{"issue":"2","key":"1063_CR65","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-021-00369-1","volume":"57","author":"A Griggio","year":"2021","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for sat-based model checking. Formal Methods Syst. Des. 57(2), 178\u2013210 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"1063_CR66","doi-asserted-by":"crossref","unstructured":"Peled, D., Zuck, L.: From model checking to a temporal proof. In: International SPIN Workshop on Model Checking of Software, pp. 1\u201314. Springer (2001)","DOI":"10.1007\/3-540-45139-0_1"},{"key":"1063_CR67","doi-asserted-by":"crossref","unstructured":"Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L.D., Ghezzi, C.: From model checking to a temporal proof for partial models. In: Software Engineering and Formal Methods (SEFM), pp. 54\u201369. Springer (2017)","DOI":"10.1007\/978-3-319-66197-1_4"},{"issue":"6","key":"1063_CR68","doi-asserted-by":"publisher","first-page":"1039","DOI":"10.1007\/s00165-021-00564-1","volume":"33","author":"C Menghi","year":"2021","unstructured":"Menghi, C., Rizzi, A.M., Bernasconi, A., Spoletini, P.: Torpedo: witnessing model correctness with topological proofs. Formal Aspects Comput. 33(6), 1039\u20131066 (2021)","journal-title":"Formal Aspects Comput."},{"key":"1063_CR69","doi-asserted-by":"crossref","unstructured":"Menghi, C., Rizzi, A.M., Bernasconi, A.: Integrating topological proofs with model checking to instrument iterative design. In: Fundamental Approaches to Software Engineering (FASE), pp. 53\u201374. Springer (2020)","DOI":"10.1007\/978-3-030-45234-6_3"},{"key":"1063_CR70","doi-asserted-by":"crossref","unstructured":"Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 362\u2013376. Springer (2006)","DOI":"10.1007\/11916277_25"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01063-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-022-01063-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-022-01063-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,25]],"date-time":"2023-09-25T02:06:34Z","timestamp":1695607594000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-022-01063-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,30]]},"references-count":70,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["1063"],"URL":"https:\/\/doi.org\/10.1007\/s10270-022-01063-4","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,30]]},"assertion":[{"value":"16 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 October 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 October 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}