{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T11:23:55Z","timestamp":1781522635429,"version":"3.54.1"},"reference-count":303,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,12,26]],"date-time":"2024-12-26T00:00:00Z","timestamp":1735171200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.<\/jats:p>","DOI":"10.1145\/3689374","type":"journal-article","created":{"date-parts":[[2024,8,21]],"date-time":"2024-08-21T23:33:30Z","timestamp":1724283210000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Formal Methods in Industry"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"first","affiliation":[{"name":"Formal Methods and Tools Lab, CNR-ISTI, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2717-760X","authenticated-orcid":false,"given":"Rod","family":"Chapman","sequence":"additional","affiliation":[{"name":"Automated Reasoning Group, Amazon Web Services, Bath, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4952-5380","authenticated-orcid":false,"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5304-8081","authenticated-orcid":false,"given":"Hubert","family":"Garavel","sequence":"additional","affiliation":[{"name":"INRIA, Grenoble, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0570-6005","authenticated-orcid":false,"given":"Rong","family":"Gu","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2655-2698","authenticated-orcid":false,"given":"Ivo","family":"ter Horst","sequence":"additional","affiliation":[{"name":"ASML, Veldhoven, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5772-9527","authenticated-orcid":false,"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8977-4827","authenticated-orcid":false,"given":"Thierry","family":"Lecomte","sequence":"additional","affiliation":[{"name":"CLEARSY Systems Engineering, Aix-en-Provence, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[{"name":"Heinrich Heine University D\u00fcsseldorf, D\u00fcsseldorf, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6593-577X","authenticated-orcid":false,"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[{"name":"Centro de Inform\u00e1tica, Universidade Federal de Pernambuco, Recife, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2870-2680","authenticated-orcid":false,"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1226-2772","authenticated-orcid":false,"given":"Martyn","family":"Thomas","sequence":"additional","affiliation":[{"name":"Gresham College, London, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3049-7962","authenticated-orcid":false,"given":"Tim A. C.","family":"Willemse","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3692-2088","authenticated-orcid":false,"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,12,26]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05032-4_17"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_3_5_2","unstructured":"Aeronautical Radio Inc. (ARINC) Airlines Electronic Engineering Committee. 2015. ARINC 653: Avionics Application Software Standard Interface Part 1 \u2014 Required Services. https:\/\/www.sae.org\/standards\/content\/arinc653p1-4\/"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-015-5346-2"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-85729-018-2_2"},{"key":"e_1_3_3_9_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-319-06200-6_3","volume-title":"Proceedings of the 6th International NASA Formal Methods Symposium (NFM\u201914)","volume":"8430","author":"Antonino Pedro R. G.","year":"2014","unstructured":"Pedro R. G. Antonino, Marcel Medeiros Oliveira, Augusto C. A. Sampaio, Klaus E. Kristensen, and Jeremy W. Bryans. 2014. Leadership election: An industrial SoS application of compositional deadlock verification. In Proceedings of the 6th International NASA Formal Methods Symposium (NFM\u201914)(LNCS, Vol. 8430), Julia M. Badger and Kristin Y. Rozier (Eds.). Springer, Germany, 31\u201345. DOI:10.1007\/978-3-319-06200-6_3"},{"key":"e_1_3_3_10_2","series-title":"Studies in Systems, Decision and Control","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-23008-0","volume-title":"Understanding Behaviour of Distributed Systems Using mCRL2","author":"Atif Muhammad","year":"2023","unstructured":"Muhammad Atif and Jan Friso Groote. 2023. Understanding Behaviour of Distributed Systems Using mCRL2. Studies in Systems, Decision and Control, Vol. 458. Springer, Germany. DOI:10.1007\/978-3-031-23008-0"},{"key":"e_1_3_3_11_2","series-title":"Mathematical Centre Tracts","volume-title":"Correctness Preserving Program Refinements: Proof Theory and Applications","author":"Back Ralph-Johan R.","year":"1980","unstructured":"Ralph-Johan R. Back. 1980. Correctness Preserving Program Refinements: Proof Theory and Applications. Mathematical Centre Tracts, Vol. 131. Mathematisch Centrum, The Netherlands."},{"key":"e_1_3_3_12_2","first-page":"1","volume-title":"Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201918)","author":"Backes John","year":"2018","unstructured":"John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper S\u00f8e Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming. 2018. Semantic-based automated reasoning for AWS access policies using SMT. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201918), Nikolaj S. Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE, USA, 1\u20139. DOI:10.23919\/FMCAD.2018.8602994"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2019.2930609"},{"key":"e_1_3_3_14_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/978-3-031-05814-1_10","volume-title":"Proceedings of the 4th International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201922)","volume":"13294","author":"Badeau Fr\u00e9d\u00e9ric","year":"2022","unstructured":"Fr\u00e9d\u00e9ric Badeau, Julien Chappelin, and Joris Lamare. 2022. Generating and verifying configuration data with OVADO. In Proceedings of the 4th International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201922)(LNCS, Vol. 13294), Simon Collart-Dutilleul, Anne E. Haxthausen, and Thierry Lecomte (Eds.). Springer, Germany, 143\u2013148. DOI:10.1007\/978-3-031-05814-1_10"},{"key":"e_1_3_3_15_2","volume-title":"The Art of Software Testing","author":"Badgett Tom","year":"2015","unstructured":"Tom Badgett, Corey Sandler, and Glenford J. Myers. 2015. The Art of Software Testing. Wiley, UK. https:\/\/www.wiley.com\/en-gb\/The+Art+of+Software+Testing%2C+3rd+Edition-p-x000565567"},{"key":"e_1_3_3_16_2","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624193","volume-title":"Process Algebra","author":"Baeten Jos C. M.","year":"1990","unstructured":"Jos C. M. Baeten and W. Peter Weijland. 1990. Process Algebra. Cambridge Tracts in Theoretical Computer Science, Vol. 18. Cambridge University Press, UK. DOI:10.1017\/CBO9780511624193"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"e_1_3_3_18_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, USA. https:\/\/mitpress.mit.edu\/9780262026499\/principles-of-model-checking\/"},{"key":"e_1_3_3_19_2","first-page":"35","volume-title":"Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201910)","author":"Ball Thomas","year":"2010","unstructured":"Thomas Ball, Ella Bounimova, Rahul Kumar, and Vladimir Levin. 2010. SLAM2: Static driver verification with under 4% false alarms. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201910), Roderick Bloem and Natasha Sharygina (Eds.). IEEE, USA, 35\u201342. https:\/\/ieeexplore.ieee.org\/document\/5770931\/"},{"key":"e_1_3_3_20_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/978-3-642-14295-6_11","volume-title":"Proceedings of the 22nd International Conference on Computer Aided Verification (CAV\u201910)","volume":"6174","author":"Ball Thomas","year":"2010","unstructured":"Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, and Jakob Lichtenberg. 2010. The static driver verifier research platform. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV\u201910)(LNCS, Vol. 6174), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.). Springer, Germany, 119\u2013122. DOI:10.1007\/978-3-642-14295-6_11"},{"key":"e_1_3_3_21_2","series-title":"LNCS","first-page":"158","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901)","volume":"2031","author":"Ball Thomas","year":"2001","unstructured":"Thomas Ball, Sagar Chaki, and Sriram K. Rajamani. 2001. Parameterized verification of multithreaded software libraries. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901)(LNCS, Vol. 2031), Tiziana Margaria and Wang Yi (Eds.). Springer, Germany, 158\u2013173. DOI:10.1007\/3-540-45319-9_12"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-019-00511-9"},{"key":"e_1_3_3_24_2","first-page":"345","volume-title":"Proceedings of the 3rd IFIP TC6\/WG6.1 International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201990)","author":"Baptista M\u00e1rio","year":"1991","unstructured":"M\u00e1rio Baptista, Susanne Graf, Jean-Luc Richier, Lu\u00eds E. T. Rodrigues, Carlos Rodriguez, Paulo Ver\u00edssimo, and Jacques Voiron. 1991. Formal specification and verification of a network independent atomic multicast protocol. In Proceedings of the 3rd IFIP TC6\/WG6.1 International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201990), Juan Quemada, Jos\u00e9 A. Ma\u00f1as, and Enrique V\u00e1zquez (Eds.). North-Holland, The Netherlands, 345\u2013352."},{"key":"e_1_3_3_25_2","series-title":"LNCS","first-page":"415","volume-title":"Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201922)","volume":"13243","author":"Barbosa Haniel","year":"2022","unstructured":"Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A versatile and industrial-strength SMT solver. In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201922)(LNCS, Vol. 13243), Dana Fisman and Grigore Rosu (Eds.). Springer, Germany, 415\u2013442. DOI:10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_3_26_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)","volume":"6806","author":"Barrett Clark W.","year":"2011","unstructured":"Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)(LNCS, Vol. 6806), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Germany, 171\u2013177. DOI:10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_3_3_28_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification: Introductory and Advanced Topics","author":"Bartocci Ezio","year":"2018","unstructured":"Ezio Bartocci and Yli\u00e8s Falcone (Eds.). 2018. Lectures on Runtime Verification: Introductory and Advanced Topics. LNCS, Vol. 10457. Springer, Germany. DOI:10.1007\/978-3-319-75632-5"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00556-1"},{"key":"e_1_3_3_30_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/978-3-319-98938-9_2","volume-title":"Proceedings of the 14th International Conference on Integrated Formal Methods (iFM\u201918)","volume":"11023","author":"Basile Davide","year":"2018","unstructured":"Davide Basile, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, Andrea Piattino, Daniele Trentini, and Alessio Ferrari. 2018. On the industrial uptake of formal methods in the railway domain. In Proceedings of the 14th International Conference on Integrated Formal Methods (iFM\u201918)(LNCS, Vol. 11023), Carlo A. Furia and Kirsten Winter (Eds.). Springer, Germany, 20\u201329. DOI:10.1007\/978-3-319-98938-9_2"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00653-3"},{"key":"e_1_3_3_32_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-030-53291-8_3","volume-title":"Proceedings of the 32nd International Conference on Computer Aided Verification (CAV\u201920)","volume":"12225","author":"Baumeister Jan","year":"2020","unstructured":"Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger, and Christoph Torens. 2020. RTLola cleared for take-off: Monitoring autonomous aircraft. In Proceedings of the 32nd International Conference on Computer Aided Verification (CAV\u201920)(LNCS, Vol. 12225), Shuvendu K. Lahiri and Chao Wang (Eds.). Springer, Germany, 28\u201339. DOI:10.1007\/978-3-030-53291-8_3"},{"key":"e_1_3_3_33_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-031-63790-2_1","volume-title":"Proceedings of the 10th International Conference on Rigorous State Based Methods (ABZ\u201924)","volume":"14759","author":"Beek Maurice H. ter","year":"2024","unstructured":"Maurice H. ter Beek. 2024. Formal methods and tools applied in the railway domain. In Proceedings of the 10th International Conference on Rigorous State Based Methods (ABZ\u201924)(LNCS, Vol. 14759), Silvia Bonfanti, Angelo Gargantini, Michael Leuschel, Elvinia Riccobene, and Patrizia Scandurra (Eds.). Springer, Germany, 3\u201321. DOI:10.1007\/978-3-031-63790-2_1"},{"key":"e_1_3_3_34_2","series-title":"LNCS","first-page":"762","volume-title":"Proceedings of the 3rd World Congress on Formal Methods: The Next 30 Years (FM\u201919)","volume":"11800","author":"Beek Maurice H. ter","year":"2019","unstructured":"Maurice H. ter Beek, Arne Bor\u00e4lv, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Christer L\u00f6fving, and Franco Mazzanti. 2019. Adopting formal methods in an industrial setting: The railways case. In Proceedings of the 3rd World Congress on Formal Methods: The Next 30 Years (FM\u201919)(LNCS, Vol. 11800), Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N. Oliveira (Eds.). Springer, Germany, 762\u2013772. DOI:10.1007\/978-3-030-30942-8_46"},{"key":"e_1_3_3_35_2","article-title":"CS2023: The role of formal methods in computer science education","author":"Beek Maurice H. ter","year":"2024","unstructured":"Maurice H. ter Beek, Manfred Broy, and Brijesh Dongol. 2024. CS2023: The role of formal methods in computer science education. ACM InRoads (2024).","journal-title":"ACM InRoads"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.3390\/software1040017"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0487-4"},{"key":"e_1_3_3_38_2","series-title":"LNCS","first-page":"369","volume-title":"Proceedings of the 1st World Congress on Formal Methods in the Development of Computing Systems (FM\u201999)","volume":"1708","author":"Behm Patrick","year":"1999","unstructured":"Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. 1999. M\u00e9t\u00e9or: A successful application of B in a large project. In Proceedings of the 1st World Congress on Formal Methods in the Development of Computing Systems (FM\u201999)(LNCS, Vol. 1708), Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.). Springer, Germany, 369\u2013387. DOI:10.1007\/3-540-48119-2_22"},{"key":"e_1_3_3_39_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907)","volume":"4590","author":"Behrmann Gerd","year":"2007","unstructured":"Gerd Behrmann, Agn\u00e8s Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. 2007. UPPAAL-Tiga: Time for playing games!. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907)(LNCS, Vol. 4590), Werner Damm and Holger Hermanns (Eds.). Springer, Germany, 121\u2013125. DOI:10.1007\/978-3-540-73368-3_14"},{"key":"e_1_3_3_40_2","first-page":"125","volume-title":"Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QEST\u201906)","author":"Behrmann Gerd","year":"2006","unstructured":"Gerd Behrmann, Alexandre David, Kim G. Larsen, John H\u00e5kansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. 2006. UPPAAL 4.0. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems (QEST\u201906). IEEE, USA, 125\u2013126. DOI:10.1109\/QEST.2006.59"},{"key":"e_1_3_3_41_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-031-43681-9_2","volume-title":"Proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201923)","volume":"14290","author":"Belli Dimitri","year":"2023","unstructured":"Dimitri Belli, Alessandro Fantechi, Stefania Gnesi, Laura Masullo, Frando Mazzanti, Lisa Quadrini, Daniele Trentini, and Carlo Vaghi. 2023. The 4SECURail case study on rigorous standard interface specifications. In Proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201923)(LNCS, Vol. 14290), Alessandro Cimatti and Laura Titolo (Eds.). Springer, Germany, 22\u201339. DOI:10.1007\/978-3-031-43681-9_2"},{"key":"e_1_3_3_42_2","first-page":"1","volume-title":"Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods in Software Engineering (FormaliSE\u201921)","author":"Belmonte Gina","year":"2021","unstructured":"Gina Belmonte, Giovanna Broccia, Vincenzo Ciancia, Diego Latella, and Mieke Massink. 2021. Feasibility of spatial model checking for nevus segmentation. In Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods in Software Engineering (FormaliSE\u201921). IEEE, USA, 1\u201312. DOI:10.1109\/FormaliSE52586.2021.00007"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10334-017-0634-z"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7"},{"key":"e_1_3_3_45_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/11757283","volume-title":"Formal Methods for Hardware Verification: Advanced Lectures of the 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201906)","author":"Bernardo Marco","year":"2006","unstructured":"Marco Bernardo and Alessandro Cimatti (Eds.). 2006. Formal Methods for Hardware Verification: Advanced Lectures of the 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201906). LNCS, Vol. 3965. Springer, Germany. DOI:10.1007\/11757283"},{"key":"e_1_3_3_46_2","series-title":"LNCS","volume-title":"Formal Methods for Executable Software Models: Advanced Lectures of the 12th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201912)","author":"Bernardo Marco","year":"2012","unstructured":"Marco Bernardo, Vittorio Cortellessa, and Alfonso Pierantonio (Eds.). 2012. Formal Methods for Executable Software Models: Advanced Lectures of the 12th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201912). LNCS, Vol. 7320. Springer, Germany. DOI:10.1007\/978-3-642-30982-3"},{"key":"e_1_3_3_47_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-07317-0","volume-title":"Formal Methods for Executable Software Models: Advanced Lectures of the 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201914)","author":"Bernardo Marco","year":"2014","unstructured":"Marco Bernardo, Ferruccio Damiani, Reiner H\u00e4hnle, Einar Broch Johnsen, and Ina Schaefer (Eds.). 2014. Formal Methods for Executable Software Models: Advanced Lectures of the 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201914). LNCS, Vol. 8483. Springer, Germany. DOI:10.1007\/978-3-319-07317-0"},{"key":"e_1_3_3_48_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-72522-0","volume-title":"Formal Methods for Performance Evaluation: Advanced Lectures of the 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201907)","author":"Bernardo Marco","year":"2007","unstructured":"Marco Bernardo and Jane Hillston (Eds.). 2007. Formal Methods for Performance Evaluation: Advanced Lectures of the 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201907). LNCS, Vol. 4486. Springer, Germany. DOI:10.1007\/978-3-540-72522-0"},{"key":"e_1_3_3_49_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-34096-8","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems: Advanced Lectures of the 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201916)","author":"Bernardo Marco","year":"2016","unstructured":"Marco Bernardo, Rocco De Nicola, and Jane Hillston (Eds.). 2016. Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems: Advanced Lectures of the 16th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM\u201916). LNCS, Vol. 9700. Springer, Germany. DOI:10.1007\/978-3-319-34096-8"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00015-5"},{"key":"e_1_3_3_51_2","first-page":"85","volume-title":"Proceedings of the ICSE 2007 Workshop on the Future of Software Engineering (FoSE\u201907)","author":"Bertolino Antonia","year":"2007","unstructured":"Antonia Bertolino. 2007. Software testing research: Achievements, challenges, dreams. In Proceedings of the ICSE 2007 Workshop on the Future of Software Engineering (FoSE\u201907), Lionel C. Briand and Alexander L. Wolf (Eds.). IEEE, USA, 85\u2013103. DOI:10.1109\/FOSE.2007.25"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-007-0008-2"},{"key":"e_1_3_3_54_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-540-24617-6_7","volume-title":"Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software (FATES\u201903)","volume":"2931","author":"Bijl Machiel van der","year":"2003","unstructured":"Machiel van der Bijl, Arend Rensink, and Jan Tretmans. 2003. Compositional testing with ioco. In Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software (FATES\u201903)(LNCS, Vol. 2931), Alexandre Petrenko and Andreas Ulrich (Eds.). Springer, Germany, 86\u2013100. DOI:10.1007\/978-3-540-24617-6_7"},{"key":"e_1_3_3_55_2","unstructured":"Lewis Binns. 2023. By Computers for Computers: Improving Scanner Metrology Software with Generated Code. https:\/\/www.linkedin.com\/pulse\/computers-improving-scanner-metrology-software-code-lewis\/"},{"key":"e_1_3_3_56_2","series-title":"LNCS","first-page":"460","volume-title":"Proceedings on the 14th International Symposium on Formal Methods (FM\u201906)","volume":"4085","author":"Blazy Sandrine","year":"2006","unstructured":"Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. 2006. Formal verification of a C compiler front-end. In Proceedings on the 14th International Symposium on Formal Methods (FM\u201906)(LNCS, Vol. 4085), Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.). Springer, Germany, 460\u2013475. DOI:10.1007\/11813040_31"},{"key":"e_1_3_3_57_2","article-title":"EAST-ADL \u2013 An Architecture Description Language for Automotive Software-Intensive Systems","author":"Blom Hans","year":"2013","unstructured":"Hans Blom, Henrik L\u00f6nn, Frank Hagl, Yiannis Papadopoulos, Mark-Oliver Reiser, Carl-Johan Sj\u00f6stedt, De-Jiu Chen, and Ramin Tavakoli Kolagari. 2013. EAST-ADL \u2013 An Architecture Description Language for Automotive Software-Intensive Systems. White Paper. https:\/\/maenad.eu\/public\/conceptpresentations\/EAST-ADL_WhitePaper_M2.1.12.pdf","journal-title":"White Paper"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"e_1_3_3_59_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14335-9","volume-title":"Testing Techniques in Software Engineering: Revised Lectures of the 2nd Pernambuco Summer School on Software Engineering (PSSE\u201907)","author":"Borba Paulo","year":"2010","unstructured":"Paulo Borba, Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock (Eds.). 2010. Testing Techniques in Software Engineering: Revised Lectures of the 2nd Pernambuco Summer School on Software Engineering (PSSE\u201907). LNCS, Vol. 6153. Springer, Germany. DOI:10.1007\/978-3-642-14335-9"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511711787.018"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASYNC.2018.00021"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1996.488298"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.391826"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.35"},{"key":"e_1_3_3_66_2","series-title":"LNCS","first-page":"183","volume-title":"Proceedings of the 1st International Symposium of Formal Methods Europe (FME\u201993)","volume":"670","author":"Bowen Jonathan P.","year":"1993","unstructured":"Jonathan P. Bowen and Victoria Stavridou. 1993. The industrial take-up of formal methods in safety-critical and other areas: A perspective. In Proceedings of the 1st International Symposium of Formal Methods Europe (FME\u201993)(LNCS, Vol. 670), Jim Woodcock and Peter Gorm Larsen (Eds.). Springer, Germany, 183\u2013195. DOI:10.1007\/BFb0024646"},{"key":"e_1_3_3_67_2","series-title":"Perspectives in Computing","volume-title":"A Computational Logic Handbook","author":"Boyer Robert S.","year":"1979","unstructured":"Robert S. Boyer and J. Strother Moore. 1979. A Computational Logic Handbook. Perspectives in Computing, Vol. 23. Academic Press, USA."},{"key":"e_1_3_3_68_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Proceedings of the 28th International Conference on Computer Safety, Reliability, and Security (SAFECOMP\u201909)","volume":"5775","author":"Bozzano Marco","year":"2009","unstructured":"Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, and Marco Roveri. 2009. The COMPASS approach: Correctness, modelling and performability of aerospace systems. In Proceedings of the 28th International Conference on Computer Safety, Reliability, and Security (SAFECOMP\u201909)(LNCS, Vol. 5775), Bettina Buth, Gerd Rabe, and Till Seyfarth (Eds.). Springer, Germany, 173\u2013186. DOI:10.1007\/978-3-642-04468-7_15"},{"key":"e_1_3_3_69_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV\u201915)","volume":"9206","author":"Bozzano Marco","year":"2015","unstructured":"Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, David Jones, Greg Kimberly, Tyler Petri, Richard Robinson, and Stefano Tonetta. 2015. Formal design and safety analysis of AIR6110 wheel brake system. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV\u201915)(LNCS, Vol. 9206), Daniel Kroening and Corina S. Pasareanu (Eds.). Springer, Germany, 518\u2013535. DOI:10.1007\/978-3-319-21690-4_36"},{"key":"e_1_3_3_70_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Proceedings of the 22nd International Conference on Computer Aided Verification (CAV\u201910)","volume":"6174","author":"Brayton Robert K.","year":"2010","unstructured":"Robert K. Brayton and Alan Mishchenko. 2010. ABC: An academic industrial-strength verification tool. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV\u201910)(LNCS, Vol. 6174), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.). Springer, Germany, 24\u201340. DOI:10.1007\/978-3-642-14295-6_5"},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/36707"},{"key":"e_1_3_3_72_2","series-title":"LNCS","first-page":"427","volume-title":"Proceedings of the 25th International Symposium on Formal Methods (FM\u201923)","volume":"14000","author":"Brucker Achim D.","year":"2023","unstructured":"Achim D. Brucker and Amy Stell. 2023. Verifying feedforward neural networks for classification in Isabelle\/HOL. In Proceedings of the 25th International Symposium on Formal Methods (FM\u201923)(LNCS, Vol. 14000), Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker (Eds.). Springer, Germany, 427\u2013444. DOI:10.1007\/978-3-031-27481-7_24"},{"key":"e_1_3_3_73_2","article-title":"A Systematic Approach to Verification & Validation Using Hardware-Assisted Verification","author":"Brunet Jean-Marie","year":"2023","unstructured":"Jean-Marie Brunet. 2023. A Systematic Approach to Verification & Validation Using Hardware-Assisted Verification. Global Semiconductor Alliance. https:\/\/www.gsaglobal.org\/forums\/a-systematic-approach-to-verification-validation-using-hardware-assisted-verification","journal-title":"Global Semiconductor Alliance"},{"key":"e_1_3_3_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10270-019-00773-6"},{"key":"e_1_3_3_75_2","article-title":"Ten Years of Patch Tuesdays: Why It\u2019s Time to Move On","author":"Budd Christopher","year":"2013","unstructured":"Christopher Budd. 2013. Ten Years of Patch Tuesdays: Why It\u2019s Time to Move On. GeekWire. https:\/\/www.geekwire.com\/2013\/ten-years-patch-tuesdays-time-move\/","journal-title":"GeekWire"},{"key":"e_1_3_3_76_2","series-title":"LNCS","first-page":"21","volume-title":"Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919)","volume":"11428","author":"Bunte Olav","year":"2019","unstructured":"Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. 2019. The mCRL2 toolset for analysing concurrent systems: Improvements in expressivity and usability. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919)(LNCS, Vol. 11428), T. Vojnar and L. Zhang (Eds.). Springer, Germany, 21\u201339. DOI:10.1007\/978-3-030-17465-1_2"},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00562-3"},{"key":"e_1_3_3_78_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-030-58298-2_8","volume-title":"Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201920)","volume":"12327","author":"Butler Michael","year":"2020","unstructured":"Michael Butler, Philipp K\u00f6rner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, and Laurent Voisin. 2020. The first twenty-five years of industrial use of the B-method. In Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201920)(LNCS, Vol. 12327), Maurice H. ter Beek and Dejan Ni\u010dkovi\u0107 (Eds.). Springer, Germany, 189\u2013209. DOI:10.1007\/978-3-030-58298-2_8"},{"key":"e_1_3_3_79_2","volume-title":"The Chorus Conflict and Loss of Separation Resolution Algorithms","author":"Butler Ricky W.","year":"2013","unstructured":"Ricky W. Butler, George E. Hagen, and Jeffrey M. Maddalon. 2013. The Chorus Conflict and Loss of Separation Resolution Algorithms. Technical Report NASA\/TM\u20132013-218030. NASA. https:\/\/ntrs.nasa.gov\/citations\/20140001006"},{"key":"e_1_3_3_80_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-016-0387-X"},{"key":"e_1_3_3_81_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Proceedings of the 26th International Conference on Computer Aided Verification (CAV\u201914)","volume":"8559","author":"Cavada Roberto","year":"2014","unstructured":"Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv symbolic model checker. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV\u201914)(LNCS, Vol. 8559), Armin Biere and Roderick Bloem (Eds.). Springer, Germany, 334\u2013342. DOI:10.1007\/978-3-319-08867-9_22"},{"key":"e_1_3_3_82_2","article-title":"How to Build the Future Verification Engineers?","author":"Cerisier Fran\u00e7ois","year":"2023","unstructured":"Fran\u00e7ois Cerisier. 2023. How to Build the Future Verification Engineers? Verification Futures Conference (VF\u201923). https:\/\/www.tessolve.com\/wp-content\/uploads\/2023\/06\/2-Francois-Cerisier-2023-How-to-build-the-future-verification-engineers-Francois-Cerisier-AEDVICES-V1-1.pdf","journal-title":"Verification Futures Conference (VF\u201923)"},{"key":"e_1_3_3_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71374-4_1"},{"key":"e_1_3_3_84_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.708566"},{"key":"e_1_3_3_85_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08970-6_2","volume-title":"Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP\u201914)","volume":"8558","author":"Chapman Roderick","year":"2014","unstructured":"Roderick Chapman and Florian Schanda. 2014. Are we there yet? 20 years of industrial theorem proving with SPARK. In Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP\u201914)(LNCS, Vol. 8558), Gerwin Klein and Ruben Gamboa (Eds.). Springer, Germany, 17\u201326. DOI:10.1007\/978-3-319-08970-6_2"},{"key":"e_1_3_3_86_2","first-page":"109","volume-title":"Proceedings of the 32nd International Conference on Software Engineering (ICSE\u201910)","author":"Chiappini Angelo","year":"2010","unstructured":"Angelo Chiappini, Alessandro Cimatti, Luca Macchi, Oscar Rebollo, Marco Roveri, Angelo Susi, Stefano Tonetta, and Berardino Vittorini. 2010. Formalization and validation of a subset of the European Train Control System. In Proceedings of the 32nd International Conference on Software Engineering (ICSE\u201910). ACM, USA, 109\u2013118. DOI:10.1145\/1810295.1810312"},{"key":"e_1_3_3_87_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV\u201902)","volume":"2404","author":"Cimatti Alessandro","year":"2002","unstructured":"Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. 2002. NuSMV 2: An opensource tool for symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV\u201902)(LNCS, Vol. 2404), Ed Brinksma and Kim G. Larsen (Eds.). Springer, Germany, 359\u2013364. DOI:10.1007\/3-540-45657-0_29"},{"key":"e_1_3_3_88_2","series-title":"LNCS","first-page":"52","volume-title":"Proceedings of the 1981 Workshop on Logics of Programs","volume":"131","author":"Clarke Edmund M.","year":"1981","unstructured":"Edmund M. Clarke and E. Allen Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the 1981 Workshop on Logics of Programs(LNCS, Vol. 131), Dexter Kozen (Ed.). Springer, Germany, 52\u201371. DOI:10.1007\/BFB0025774"},{"key":"e_1_3_3_89_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_3_90_2","series-title":"LNCS","first-page":"168","volume-title":"Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904)","volume":"2988","author":"Clarke Edmund M.","year":"2004","unstructured":"Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904)(LNCS, Vol. 2988), Kurt Jensen and Andreas Podelski (Eds.). Springer, Germany, 168\u2013176. DOI:10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_3_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"key":"e_1_3_3_93_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_32"},{"key":"e_1_3_3_94_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification (CAV\u201996)","volume":"1102","author":"Cleaveland Rance","year":"1996","unstructured":"Rance Cleaveland and Steve Sims. 1996. The NCSU concurrency workbench. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV\u201996)(LNCS, Vol. 1102), Rajeev Alur and Thomas A. Henzinger (Eds.). Springer, Germany, 394\u2013397. DOI:10.1007\/3-540-61474-5_87"},{"key":"e_1_3_3_95_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-09268-8"},{"key":"e_1_3_3_96_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-030-18744-6_13","volume-title":"Proceedings of the 3rd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201919)","volume":"11495","author":"Comptier Mathieu","year":"2019","unstructured":"Mathieu Comptier, Michael Leuschel, Luis-Fernando Mejia, Julien Molinero Perez, and Mareike Mutz. 2019. Property-based modelling and validation of a CBTC zone controller in Event-B. In Proceedings of the 3rd International Conference on Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification (RSSRail\u201919)(LNCS, Vol. 11495), Simon Collart-Dutilleul, Thierry Lecomte, and Alexander B. Romanovsky (Eds.). Springer, Germany, 202\u2013212. DOI:10.1007\/978-3-030-18744-6_13"},{"key":"e_1_3_3_97_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-319-96145-3_3","volume-title":"Proceedings of the 30th International Conference on Computer Aided Verification (CAV\u201918)","volume":"10981","author":"Cook Byron","year":"2018","unstructured":"Byron Cook. 2018. Formal reasoning about the security of Amazon Web Services. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV\u201918)(LNCS, Vol. 10981), Hana Chockler and Georg Weissenbacher (Eds.). Springer, Germany, 38\u201347. DOI:10.1007\/978-3-319-96145-3_3"},{"key":"e_1_3_3_98_2","unstructured":"Byron Cook. 2022. Automated Reasoning\u2019s Scientific Frontiers. https:\/\/www.amazon.science\/blog\/automated-reasonings-scientific-frontiers"},{"key":"e_1_3_3_99_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/978-3-319-96142-2_28","volume-title":"Proceedings of the 30th International Conference on Computer Aided Verification (CAV\u201918)","volume":"10982","author":"Cook Byron","year":"2018","unstructured":"Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. 2018. Model checking boot code from AWS data centers. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV\u201918)(LNCS, Vol. 10982), Hana Chockler and Georg Weissenbacher (Eds.). Springer, Germany, 467\u2013486. DOI:10.1007\/978-3-319-96142-2_28"},{"key":"e_1_3_3_100_2","article-title":"Shiny Object Syndrome: The Biggest Problem for Today\u2019s Entrepreneurs","author":"Cook Jodie","year":"2023","unstructured":"Jodie Cook. 2023. Shiny Object Syndrome: The Biggest Problem for Today\u2019s Entrepreneurs. Forbes. https:\/\/www.forbes.com\/sites\/jodiecook\/2023\/02\/20\/shiny-object-syndrome-the-biggest-problem-for-todays-entrepreneurs\/?sh=5a90cb4b6709","journal-title":"Forbes"},{"key":"e_1_3_3_101_2","series-title":"LNCS","first-page":"151","volume-title":"Proceedings of the European Conference on Computer Algebra (EUROCAL\u201985)","volume":"203","author":"Coquand Thierry","year":"1985","unstructured":"Thierry Coquand and G\u00e9rard P. Huet. 1985. Constructions: A higher order proof system for mechanizing mathematics. In Proceedings of the European Conference on Computer Algebra (EUROCAL\u201985)(LNCS, Vol. 203), Bruno Buchberger (Ed.). Springer, Germany, 151\u2013184. DOI:10.1007\/3-540-15983-5_13"},{"key":"e_1_3_3_102_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/978-3-642-02658-4_18","volume-title":"Proceedings of the 21st International Conference on Computer Aided Verification (CAV\u201909)","volume":"5643","author":"Coste Nicolas","year":"2009","unstructured":"Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, and Wendelin Serwe. 2009. Towards performance prediction of compositional models in industrial GALS designs. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV\u201909)(LNCS, Vol. 5643), Ahmed Bouajjani and Oded Maler (Eds.). Springer, Germany, 204\u2013218. DOI:10.1007\/978-3-642-02658-4_18"},{"key":"e_1_3_3_103_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(96)00083-9"},{"key":"e_1_3_3_104_2","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press, USA. https:\/\/mitpress.mit.edu\/9780262044905\/principles-of-abstract-interpretation\/"},{"key":"e_1_3_3_105_2","doi-asserted-by":"publisher","DOI":"10.1145\/3488716"},{"key":"e_1_3_3_106_2","first-page":"1","volume-title":"Proceedings of the 53rd IEEE\/ASEE International Conference on Frontiers in Education (FIE\u201923)","author":"Junior Braz Araujo da Silva","year":"2023","unstructured":"Braz Araujo da Silva Junior, Simone Andr\u00e9 da Costa Cavalheiro, Luciana Foss, and J\u00falia Veiga da Silva. 2023. Formal specification in basic education: What does it take?. In Proceedings of the 53rd IEEE\/ASEE International Conference on Frontiers in Education (FIE\u201923). IEEE, USA, 1\u20139. DOI:10.1109\/FIE58773.2023.10343074"},{"key":"e_1_3_3_107_2","volume-title":"Proceedings of the 2021 AIAA SciTech Forum","author":"Dabney James B.","year":"2021","unstructured":"James B. Dabney, Julia M. Badger, and Pavan Rajagopal. 2021. Adding a verification view for an autonomous real-time system architecture. In Proceedings of the 2021 AIAA SciTech Forum. AIAA, USA, Article 0566, 12 pages. DOI:10.2514\/6.2021-0566"},{"key":"e_1_3_3_108_2","first-page":"57","volume-title":"Proceedings of the 14th IEEE Space Computing Conference (SCC\u201923)","author":"Dabney James B.","year":"2023","unstructured":"James B. Dabney, Julia M. Badger, and Pavan Rajagopal. 2023. Trustworthy autonomy for gateway vehicle system manager. In Proceedings of the 14th IEEE Space Computing Conference (SCC\u201923). IEEE, USA, 57\u201362. DOI:10.1109\/SCC57168.2023.00018"},{"key":"e_1_3_3_109_2","series-title":"IFIP Transactions","first-page":"199","volume-title":"Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992)","volume":"10","author":"DaSilva Clara","year":"1992","unstructured":"Clara DaSilva, Babak Dehbonei, and Fernando Mejia. 1992. Formal specification in the development of industrial applications: Subway speed control system. In Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201992)(IFIP Transactions, Vol. C-10), Michel Diaz and Roland Groz (Eds.). North-Holland, The Netherlands, 199\u2013213."},{"key":"e_1_3_3_110_2","series-title":"LNCS","first-page":"206","volume-title":"Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915)","volume":"9035","author":"David Alexandre","year":"2015","unstructured":"Alexandre David, Peter G. Jensen, Kim G. Larsen, Marius Mikucionis, and Jakob H. Taankvist. 2015. Uppaal Stratego. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915)(LNCS, Vol. 9035), Christel Baier and Cesare Tinelli (Eds.). Springer, Germany, 206\u2013211. DOI:10.1007\/978-3-662-46681-0_16"},{"key":"e_1_3_3_111_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-014-0361-Y"},{"key":"e_1_3_3_112_2","volume-title":"AADL In Practice: Design and Validate the Architecture of Critical Systems","author":"Delange Julien","year":"2017","unstructured":"Julien Delange. 2017. AADL In Practice: Design and Validate the Architecture of Critical Systems. Reblochon, France."},{"key":"e_1_3_3_113_2","series-title":"LNCS","first-page":"437","volume-title":"Proceedings of the 14th International Symposium on Static Analysis (SAS\u201907)","volume":"4634","author":"Delmas David","year":"2007","unstructured":"David Delmas and Jean Souyris. 2007. Astr\u00e9e: From research to industry. In Proceedings of the 14th International Symposium on Static Analysis (SAS\u201907)(LNCS, Vol. 4634), Hanne Riis Nielson and Gilberto Fil\u00e9 (Eds.). Springer, Germany, 437\u2013451. DOI:10.1007\/978-3-540-74061-2_27"},{"key":"e_1_3_3_114_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01933419"},{"key":"e_1_3_3_115_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall, USA."},{"key":"e_1_3_3_116_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification (CAV\u201996)","volume":"1102","author":"Dill David L.","year":"1996","unstructured":"David L. Dill. 1996. The Murphi verification system. In Proceedings of the 8th International Conference on Computer Aided Verification (CAV\u201996)(LNCS, Vol. 1102), Rajeev Alur and Thomas A. Henzinger (Eds.). Springer, Germany, 390\u2013393. DOI:10.1007\/3-540-61474-5_86"},{"key":"e_1_3_3_117_2","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_3_118_2","doi-asserted-by":"publisher","DOI":"10.3166\/tsi.22.11-32"},{"key":"e_1_3_3_119_2","doi-asserted-by":"publisher","DOI":"10.1145\/36704"},{"key":"e_1_3_3_120_2","series-title":"LNCS","first-page":"215","volume-title":"Proceedings of the 19th International Symposium on Formal Methods (FM\u201914)","volume":"8442","author":"Duggirala Parasara Sridhar","year":"2014","unstructured":"Parasara Sridhar Duggirala, Le Wang, Sayan Mitra, Mahesh Viswanathan, and C\u00e9sar A. Mu\u00f1oz. 2014. Temporal precedence checking for switched models and its application to a parallel landing protocol. In Proceedings of the 19th International Symposium on Formal Methods (FM\u201914)(LNCS, Vol. 8442), Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer, Germany, 215\u2013229. DOI:10.1007\/978-3-319-06410-9_16"},{"key":"e_1_3_3_121_2","volume-title":"Probabilistic Analysis of Distributed Fault-Tolerant Systems","author":"Dutertre Bruno","year":"2011","unstructured":"Bruno Dutertre. 2011. Probabilistic Analysis of Distributed Fault-Tolerant Systems. Technical Report NASA\/CR\u20132011-217090. NASA. https:\/\/ntrs.nasa.gov\/citations\/20110011564"},{"key":"e_1_3_3_122_2","series-title":"LNCS","first-page":"252","volume-title":"Proceedings of the 7th International Conference of B Users (B\u201907)","volume":"4355","author":"Essam\u00e9 Didier","year":"2007","unstructured":"Didier Essam\u00e9 and Daniel Doll\u00e9. 2007. B in large scale projects: The Canarsie Line CBTC experience. In Proceedings of the 7th International Conference of B Users (B\u201907)(LNCS, Vol. 4355), Jacques Julliand and Olga Kouchnarenko (Eds.). Springer, Germany, 252\u2013254. DOI:10.1007\/11955757_21"},{"key":"e_1_3_3_123_2","unstructured":"European Committee for Electrotechnical Standardization. 2011. CENELEC EN 50128: Railway Applications \u2013 Communication Signalling and Processing Systems \u2013 Software for Railway Control and Protection Systems. https:\/\/standards.globalspec.com\/std\/1678027\/cenelec-en-50128"},{"key":"e_1_3_3_124_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-030-98464-9_9","volume-title":"Proceedings of the 28th International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ\u201922)","volume":"13216","author":"Farrell Marie","year":"2022","unstructured":"Marie Farrell, Matt Luckcuck, Ois\u00edn Sheridan, and Rosemary Monahan. 2022. FRETting about requirements: Formalised requirements for an aircraft engine controller. In Proceedings of the 28th International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ\u201922)(LNCS, Vol. 13216), Vincenzo Gervasi and Andreas Vogelsang (Eds.). Springer, Germany, 96\u2013111. DOI:10.1007\/978-3-030-98464-9_9"},{"key":"e_1_3_3_125_2","first-page":"555","volume-title":"Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS\u201917)","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Rui Xu, Danfeng Zhang, Andrew C. Myers, and G. Edward Suh. 2017. Verification of a practical hardware security architecture through static information flow analysis. In Proceedings of the 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS\u201917), Yunji Chen, Olivier Temam, and John Carter (Eds.). ACM, USA, 555\u2013568. DOI:10.1145\/3037697.3037739"},{"key":"e_1_3_3_126_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.04.003"},{"key":"e_1_3_3_127_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3124677"},{"key":"e_1_3_3_128_2","first-page":"62","volume-title":"Proceedings of the 42nd International Conference on Software Engineering (ICSE\u201920)","author":"Ferrari Alessio","year":"2020","unstructured":"Alessio Ferrari, Franco Mazzanti, Davide Basile, Maurice H. ter Beek, and Alessandro Fantechi. 2020. Comparing formal tools for system design: A judgment study. In Proceedings of the 42nd International Conference on Software Engineering (ICSE\u201920). ACM, USA, 62\u201374. DOI:10.1145\/3377811.3380373"},{"key":"e_1_3_3_129_2","doi-asserted-by":"publisher","DOI":"10.1145\/3520480"},{"key":"e_1_3_3_130_2","article-title":"TaRGeT: A Model Based Product Line Testing Tool","author":"Ferreira Felype","year":"2010","unstructured":"Felype Ferreira, La\u00eds Neves, Michelle Silva, and Paulo Borba. 2010. TaRGeT: A Model Based Product Line Testing Tool. Tools Session of the 1st Brazilian Conference on Software: Theory and Practice (CBSoft\u201910). https:\/\/twiki.cin.ufpe.br\/twiki\/pub\/SPG\/SoftwareEstimationModels\/TargetCBSOFT.pdf","journal-title":"Tools Session of the 1st Brazilian Conference on Software: Theory and Practice (CBSoft\u201910)"},{"key":"e_1_3_3_131_2","first-page":"1","volume-title":"Proceedings of the 13th ACM\/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM\u201919)","author":"Ferreira Larissa","year":"2019","unstructured":"Larissa Ferreira, Sidney C. Nogueira, Lucas Lima, Liliane Fonseca, and Waldemar Ferreira. 2019. Initial findings on the evaluation of a model-based testing tool in the test design process. In Proceedings of the 13th ACM\/IEEE International Symposium on Empirical Software Engineering and Measurement (ESEM\u201919). IEEE, USA, 1\u20136. DOI:10.1109\/ESEM.2019.8870140"},{"key":"e_1_3_3_132_2","series-title":"LNCS","first-page":"748","volume-title":"Proceedings of the 21st International Symposium on Formal Methods (FM\u201916)","volume":"9995","author":"Filipovikj Predrag","year":"2016","unstructured":"Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz, and Henrik L\u00f6nn. 2016. Simulink to UPPAAL statistical model checker: Analyzing automotive industrial systems. In Proceedings of the 21st International Symposium on Formal Methods (FM\u201916)(LNCS, Vol. 9995), John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer, Germany, 748\u2013756. DOI:10.1007\/978-3-319-48989-6_46"},{"key":"e_1_3_3_133_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-020-09487-2"},{"key":"e_1_3_3_134_2","series-title":"Mathematical Aspects of Computer Science","first-page":"19","volume-title":"Proceedings of Symposia in Applied Mathematics","volume":"19","author":"Floyd Robert W.","year":"1967","unstructured":"Robert W. Floyd. 1967. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics(Mathematical Aspects of Computer Science, Vol. 19), J. T. Schwartz (Ed.). American Mathematical Society, USA, 19\u201332."},{"key":"e_1_3_3_135_2","series-title":"LNCS","first-page":"741","volume-title":"Proceedings of the 24th International Symposium on Formal Methods (FM\u201921)","volume":"13047","author":"Gao Song","year":"2021","unstructured":"Song Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, and Lijun Zhang. 2021. Formal verification of consensus in the Taurus distributed database. In Proceedings of the 24th International Symposium on Formal Methods (FM\u201921)(LNCS, Vol. 13047), Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan (Eds.). Springer, Germany, 741\u2013751. DOI:10.1007\/978-3-030-90870-6_42"},{"key":"e_1_3_3_136_2","volume-title":"Formal Methods for Safe and Secure Computer Systems","author":"Garavel Hubert","year":"2013","unstructured":"Hubert Garavel and Susanne Graf. 2013. Formal Methods for Safe and Secure Computer Systems. BSI Study 875. Bundesamt f\u00fcr Sicherheit in der Informationstechnik. https:\/\/www.bsi.bund.de\/SharedDocs\/Downloads\/DE\/BSI\/Publikationen\/Studien\/formal_methods_study_875\/formal_methods_study_875.html"},{"key":"e_1_3_3_137_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_3_3_138_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68270-9_1"},{"key":"e_1_3_3_139_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","volume-title":"Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201920)","volume":"12327","author":"Garavel Hubert","year":"2020","unstructured":"Hubert Garavel, Maurice H. ter Beek, and Jaco van de Pol. 2020. The 2020 expert survey on formal methods. In Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201920)(LNCS, Vol. 12327), Maurice H. ter Beek and Dejan Ni\u010dkovi\u0107 (Eds.). Springer, Germany, 3\u201369. DOI:10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_3_140_2","series-title":"LNCS","first-page":"3","volume-title":"Proceedings of the 28th International Conference on Computer Aided Verification (CAV\u201916)","volume":"9780","author":"Gario Marco","year":"2016","unstructured":"Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, and Kristin Y. Rozier. 2016. Model checking at scale: Automated air traffic control design space exploration. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV\u201916)(LNCS, Vol. 9780), Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer, Germany, 3\u201322. DOI:10.1007\/978-3-319-41540-6_1"},{"key":"e_1_3_3_141_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/BFb0012879","volume-title":"Proceedings of the 9th International Conference on Automated Deduction (CADE\u201988)","volume":"310","author":"Garland Stephen J.","year":"1988","unstructured":"Stephen J. Garland and John V. Guttag. 1988. LP: The larch prover. In Proceedings of the 9th International Conference on Automated Deduction (CADE\u201988)(LNCS, Vol. 310), Ewing L. Lusk and Ross A. Overbeek (Eds.). Springer, Germany, 748\u2013749. DOI:10.1007\/BFB0012879"},{"key":"e_1_3_3_142_2","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1145\/2642937.2642940","volume-title":"Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE\u201914)","author":"Giannakopoulou Dimitra","year":"2014","unstructured":"Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Todd Lauderdale, Zvonimir Rakamaric, and Vishwanath Raman. 2014. Taming test inputs for separation assurance. In Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering (ASE\u201914). ACM, USA, 373\u2013384. DOI:10.1145\/2642937.2642940"},{"key":"e_1_3_3_143_2","series-title":"CEUR Proceedings","first-page":"6","volume-title":"Joint Proceedings of the Co-Located Events of the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-JP\u201920)","volume":"2584","author":"Giannakopoulou Dimitra","year":"2020","unstructured":"Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Julian Rhein, Johann Schumann, and Nija Shi. 2020. Formal requirements elicitation with FRET. In Joint Proceedings of the Co-Located Events of the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-JP\u201920)(CEUR Proceedings, Vol. 2584), Mehrdad Sabetzadeh, Andreas Vogelsang, Sallam Abualhaija, Markus Borg, Fabiano Dalpiaz, Maya Daneva, Nelly Condori-Fern\u00e1ndez, Xavier Franch, Davide Fucci, Vincenzo Gervasi, Eduard C. Groen, Renata S. S. Guizzardi, Andrea Herrmann, Jennifer Horkoff, Luisa Mich, Anna Perini, and Angelo Susi (Eds.). CEUR-WS.org, Germany, 6 pages. https:\/\/ceur-ws.org\/Vol-2584\/PT-paper4.pdf"},{"key":"e_1_3_3_144_2","series-title":"LNCS","first-page":"187","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914)","volume":"8413","author":"Gibson-Robinson Thomas","year":"2014","unstructured":"Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, and A. W. Roscoe. 2014. FDR3 \u2013 a modern refinement checker for CSP. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914)(LNCS, Vol. 8413), Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer, Germany, 187\u2013201. DOI:10.1007\/978-3-642-54862-8_13"},{"key":"e_1_3_3_145_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09836-5"},{"key":"e_1_3_3_146_2","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898"},{"key":"e_1_3_3_147_2","doi-asserted-by":"publisher","DOI":"10.1145\/3363824"},{"key":"e_1_3_3_148_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2008.109"},{"key":"e_1_3_3_149_2","series-title":"LNCS","first-page":"112","volume-title":"Proceedings of the 18th International Symposium on Static Analysis (SAS\u201911)","volume":"6887","author":"Godefroid Patrice","year":"2011","unstructured":"Patrice Godefroid, Shuvendu K. Lahiri, and Cindy Rubio-Gonz\u00e1lez. 2011. Statically validating must summaries for incremental compositional dynamic test generation. In Proceedings of the 18th International Symposium on Static Analysis (SAS\u201911)(LNCS, Vol. 6887), Eran Yahav (Ed.). Springer, Germany, 112\u2013128. DOI:10.1007\/978-3-642-23702-7_12"},{"key":"e_1_3_3_150_2","first-page":"16","volume-title":"Proceedings of the 15th Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated whitebox fuzz testing. In Proceedings of the 15th Network and Distributed System Security Symposium (NDSS\u201908). The Internet Society, USA, 16 pages. https:\/\/www.ndss-symposium.org\/ndss2008\/automated-whitebox-fuzz-testing\/"},{"key":"e_1_3_3_151_2","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_3_152_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-012-0238-X"},{"key":"e_1_3_3_153_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"Gordon Michael J.","year":"1979","unstructured":"Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. 1979. Edinburgh LCF: A Mechanised Logic of Computation. LNCS, Vol. 78. Springer, Germany. DOI:10.1007\/3-540-09724-4"},{"key":"e_1_3_3_154_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-017-9426-4"},{"key":"e_1_3_3_155_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Proceedings of the 27th International Conference on Computer Aided Verification (CAV\u201915)","volume":"9206","author":"Gouw Stijn de","year":"2015","unstructured":"Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, and Reiner H\u00e4hnle. 2015. OpenJDK\u2019s Java.utils.Collection.sort() is broken: The good, the bad and the worst case. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV\u201915)(LNCS, Vol. 9206), Daniel Kroening and Corina S. Pasareanu (Eds.). Springer, Germany, 273\u2013289. DOI:10.1007\/978-3-319-21690-4_16"},{"key":"e_1_3_3_156_2","volume-title":"Proceedings of the 17th Systems and Software Technology Conference (SSTC\u201905)","author":"Greve David","year":"2005","unstructured":"David Greve, Matthew Wilding, and W. Mark Vanfleet. 2005. High assurance formal security policy modeling. In Proceedings of the 17th Systems and Software Technology Conference (SSTC\u201905). IEEE, USA."},{"key":"e_1_3_3_157_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-014-9408-8"},{"key":"e_1_3_3_158_2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"Groote Jan Friso","year":"2014","unstructured":"Jan Friso Groote and Mohammad Reza Mousavi. 2014. Modeling and Analysis of Communicating Systems. MIT Press, USA. https:\/\/mitpress.mit.edu\/9780262547871\/modeling-and-analysis-of-communicating-systems\/"},{"key":"e_1_3_3_159_2","series-title":"LNCS","first-page":"186","volume-title":"Proceedings of the 11th International NASA Formal Methods Symposium (NFM\u201919)","volume":"11460","author":"Gu Rong","year":"2019","unstructured":"Rong Gu, Raluca Marinescu, Cristina Seceleanu, and Kristina Lundqvist. 2019. Towards a two-layer framework for verifying autonomous vehicles. In Proceedings of the 11th International NASA Formal Methods Symposium (NFM\u201919)(LNCS, Vol. 11460), Julia M. Badger and Kristin Yvonne Rozier (Eds.). Springer, Germany, 186\u2013203. DOI:10.1007\/978-3-030-20652-9_12"},{"key":"e_1_3_3_160_2","first-page":"186","volume-title":"Proceedings of the 12th International Conference on Software Engineering (ICSE\u201990)","author":"Guiho G\u00e9rard","year":"1990","unstructured":"G\u00e9rard Guiho and Claude Hennebert. 1990. SACEM software validation. In Proceedings of the 12th International Conference on Software Engineering (ICSE\u201990). IEEE, USA, 186\u2013191."},{"key":"e_1_3_3_161_2","volume-title":"Proceedings of the 11th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference","author":"Hagen George","year":"2011","unstructured":"George Hagen, Ricky Butler, and Jeffrey Maddalon. 2011. Stratway: A modular approach to strategic conflict resolution. In Proceedings of the 11th AIAA Aviation Technology, Integration, and Operations (ATIO) Conference. AIAA, USA, Article 6892, 13 pages. DOI:10.2514\/6.2011-6892"},{"key":"e_1_3_3_162_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"e_1_3_3_163_2","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-013-05-0669"},{"key":"e_1_3_3_164_2","doi-asserted-by":"publisher","DOI":"10.1007\/b97644"},{"key":"e_1_3_3_165_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00551-6"},{"key":"e_1_3_3_166_2","first-page":"11","volume-title":"Proceedings of the 6th International Workshop on the ACL2 Prover and its Applications (ACL2\u201906)","author":"Hardin David S.","year":"2006","unstructured":"David S. Hardin, Eric W. Smith, and William D. Young. 2006. A robust machine code proof framework for highly secure applications. In Proceedings of the 6th International Workshop on the ACL2 Prover and its Applications (ACL2\u201906). ACM, USA, 11\u201320. DOI:10.1145\/1217975.1217978"},{"key":"e_1_3_3_167_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_3_3_168_2","unstructured":"John Harrison. 2023. s2n-bignum GitHub Repository. https:\/\/github.com\/awslabs\/s2n-bignum"},{"key":"e_1_3_3_169_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-022-00679-7"},{"key":"e_1_3_3_170_2","doi-asserted-by":"publisher","DOI":"10.1145\/1459352.1459354"},{"key":"e_1_3_3_171_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_172_2","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R. (Tony)","year":"1985","unstructured":"C. A. R. (Tony) Hoare. 1985. Communicating Sequential Processes. Prentice Hall, USA."},{"key":"e_1_3_3_173_2","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann Gerard J.","year":"2003","unstructured":"Gerard J. Holzmann. 2003. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, USA."},{"key":"e_1_3_3_174_2","doi-asserted-by":"publisher","DOI":"10.1145\/2560217.2560218"},{"key":"e_1_3_3_175_2","unstructured":"Marieke Huisman Dilian Gurov and Alexander Malkis. 2020. Formal Methods: From Academia to Industrial Practice \u2013 A Travel Guide. arxiv:2002.07279"},{"key":"e_1_3_3_176_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30167-4"},{"key":"e_1_3_3_177_2","article-title":"Intel Identifies Chipset Design Error, Implementing Solution","year":"2011","unstructured":"Intel. 2011. Intel Identifies Chipset Design Error, Implementing Solution. Press release. https:\/\/intc.com\/news-events\/press-releases\/detail\/688\/intel-identifies-chipset-design-error-implementing-solution","journal-title":"Press release"},{"key":"e_1_3_3_178_2","unstructured":"International Electrotechnical Commission. 2023. IEC TC 107: Process Management for Avionics. https:\/\/www.iec.ch\/dyn\/www\/f?p=103:7:0::::FSP_ORG_ID:1304"},{"key":"e_1_3_3_179_2","unstructured":"International Electrotechnical Commission. 2023. IEC TC 97: Electrical Installations for Lighting and Beaconing of Aerodromes. https:\/\/www.iec.ch\/dyn\/www\/f?p=103:7:0::::FSP_ORG_ID:1294"},{"key":"e_1_3_3_180_2","unstructured":"International Organization for Standardization. 2018. ISO 26262: Road Vehicles \u2014 Functional Safety \u2014 Parts 1\u201312. https:\/\/www.iso.org\/standard\/68383.html"},{"key":"e_1_3_3_181_2","unstructured":"International Organization for Standardization and International Electrotechnical Commission. 2017. ISO\/IEC 19514 - Information Technology \u2013 Object Management Group Systems Modeling Language (OMG SysML). https:\/\/www.iso.org\/standard\/65231.html"},{"key":"e_1_3_3_182_2","volume-title":"The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling","author":"Jain Raj","year":"1991","unstructured":"Raj Jain. 1991. The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling. Wiley, UK. https:\/\/www.wiley.com\/en-us\/The+Art+of+Computer+Systems+Performance+Analysis%3A+Techniques+for+Experimental+Design%2C+Measurement%2C+Simulation%2C+and+Modeling-p-9780471503361"},{"key":"e_1_3_3_183_2","series-title":"LNCS","first-page":"21","volume-title":"Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915)","volume":"9035","author":"Jeannin Jean-Baptiste","year":"2015","unstructured":"Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan W. Gardner, Aurora C. Schmidt, Erik Zawadzki, and Andr\u00e9 Platzer. 2015. A formally verified hybrid system for the next-generation airborne collision avoidance system. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915)(LNCS, Vol. 9035), Christel Baier and Cesare Tinelli (Eds.). Springer, Germany, 21\u201336. DOI:10.1007\/978-3-662-46681-0_2"},{"key":"e_1_3_3_184_2","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1145\/3314221.3314595","volume-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201919)","author":"Jiang Hanru","year":"2019","unstructured":"Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, and Xinyu Feng. 2019. Towards certified separate compilation for concurrent programs. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201919). ACM, USA, 111\u2013125. DOI:10.1145\/3314221.3314595"},{"key":"e_1_3_3_185_2","first-page":"171","volume-title":"A Classical Mind: Essays in Honour of C. A. R. Hoare","author":"Jifeng He","year":"1994","unstructured":"He Jifeng. 1994. From CSP to hybrid systems. In A Classical Mind: Essays in Honour of C. A. R. Hoare, A. W. (Bill) Roscoe (Ed.). Prentice Hall, UK, 171\u2013189."},{"key":"e_1_3_3_186_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/978-3-031-37709-9_23","volume-title":"Proceedings of the 35th International Conference on Computer Aided Verification (CAV\u201923)","volume":"13966","author":"Johannsen Chris","year":"2023","unstructured":"Chris Johannsen, Phillip H. Jones, Brian Kempa, Kristin Y. Rozier, and Pei Zhang. 2023. R2U2 version 3.0: Re-Imagining a toolchain for specification, resource estimation, and optimized observer generation for runtime verification in hardware and software. In Proceedings of the 35th International Conference on Computer Aided Verification (CAV\u201923)(LNCS, Vol. 13966), Constantin Enea and Akash Lal (Eds.). Springer, Germany, 483\u2013497. 10.1007\/978-3-031-37709-9_23"},{"key":"e_1_3_3_187_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-031-43681-9_9","volume-title":"Proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201923)","volume":"14290","author":"Johannsen Chris","year":"2023","unstructured":"Chris Johannsen, Brian Kempa, Phillip H. Jones, Kristin Y. Rozier, and Tichakorn Wongpiromsarn. 2023. Impossible made possible: Encoding intractable specifications via implied domain constraints. In Proceedings of the 28th International Conference on Formal Methods for Industrial Critical Systems (FMICS\u201923)(LNCS, Vol. 14290), Alessandro Cimatti and Laura Titolo (Eds.). Springer, Germany, 151\u2013169. DOI:10.1007\/978-3-031-43681-9_9"},{"key":"e_1_3_3_188_2","volume-title":"Lint, a C Program Checker","author":"Johnson Stephen C.","year":"1977","unstructured":"Stephen C. Johnson. 1977. Lint, a C Program Checker. Technical Report 65. Bell Labs."},{"key":"e_1_3_3_189_2","volume-title":"Systematic Software Development using VDM (2 ed.)","author":"Jones Clifford B.","year":"1991","unstructured":"Clifford B. Jones. 1991. Systematic Software Development using VDM (2 ed.). Prentice Hall, USA."},{"key":"e_1_3_3_190_2","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_3_3_191_2","series-title":"Advances in Formal Methods","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann Matt","year":"2000","unstructured":"Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore. 2000. Computer-Aided Reasoning: An Approach. Advances in Formal Methods, Vol. 3. Springer, Germany. DOI:10.1007\/978-1-4615-4449-4"},{"key":"e_1_3_3_192_2","series-title":"Advances in Formal Methods","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"Kaufmann Matt","year":"2000","unstructured":"Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore (Eds.). 2000. Computer-Aided Reasoning: ACL2 Case Studies. Advances in Formal Methods, Vol. 4. Springer, Germany. DOI:10.1007\/978-1-4757-3188-0"},{"key":"e_1_3_3_193_2","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_3_194_2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP\u201909)","author":"Klein Gerwin","year":"2009","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP\u201909), Jeanna Neefe Matthews and Thomas E. Anderson (Eds.). ACM, USA, 207\u2013220. DOI:10.1145\/1629575.1629596"},{"key":"e_1_3_3_195_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-319-46982-9_7","volume-title":"Proceedings of the 16th International Conference on Runtime Verification (RV\u201916)","volume":"10012","author":"Kosmatov Nikolai","year":"2016","unstructured":"Nikolai Kosmatov and Julien Signoles. 2016. Frama-C, A collaborative framework for C code verification: Tutorial synopsis. In Proceedings of the 16th International Conference on Runtime Verification (RV\u201916)(LNCS, Vol. 10012), Yli\u00e8s Falcone and C\u00e9sar S\u00e1nchez (Eds.). Springer, Germany, 92\u2013115. DOI:10.1007\/978-3-319-46982-9_7"},{"key":"e_1_3_3_196_2","doi-asserted-by":"publisher","DOI":"10.4230\/DAGMAN.1.1.21"},{"key":"e_1_3_3_197_2","series-title":"LNCS","first-page":"708","volume-title":"Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915)","volume":"9035","author":"Kriouile Abderahman","year":"2015","unstructured":"Abderahman Kriouile and Wendelin Serwe. 2015. Using a formal model to improve verification of a cache-coherent system-on-chip. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915)(LNCS, Vol. 9035), Christel Baier and Cesare Tinelli (Eds.). Springer, Germany, 708\u2013722. DOI:10.1007\/978-3-662-46681-0_62"},{"key":"e_1_3_3_198_2","doi-asserted-by":"publisher","DOI":"10.1145\/3664191"},{"key":"e_1_3_3_199_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_3_3_200_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)","volume":"6806","author":"Kwiatkowska Marta Z.","year":"2011","unstructured":"Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)(LNCS, Vol. 6806), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, Germany, 585\u2013591. DOI:10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_3_201_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-028-4-126"},{"key":"e_1_3_3_202_2","first-page":"174","volume-title":"Proceedings of the 7th ACM Symposium on Principles of Programming Languages (POPL\u201980)","author":"Lamport Leslie","year":"1980","unstructured":"Leslie Lamport. 1980. \u201cSometime\u201d is sometimes \u201cnot never\u201d: On the temporal logic of programs. In Proceedings of the 7th ACM Symposium on Principles of Programming Languages (POPL\u201980). ACM, USA, 174\u2013185. DOI:10.1145\/567446.567463"},{"key":"e_1_3_3_203_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.01.003"},{"key":"e_1_3_3_204_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/978-3-642-38088-4_19","volume-title":"Proceedings of the 5th International NASA Formal Methods Symposium (NFM\u201913)","volume":"7871","author":"Larson Brian R.","year":"2013","unstructured":"Brian R. Larson, Patrice Chalin, and John Hatcliff. 2013. BLESS: Formal specification and verification of behaviors for embedded systems with software. In Proceedings of the 5th International NASA Formal Methods Symposium (NFM\u201913)(LNCS, Vol. 7871), Guillaume Brat, Neha Rungta, and Arnaud Venet (Eds.). Springer, Germany, 276\u2013290. DOI:10.1007\/978-3-642-38088-4_19"},{"key":"e_1_3_3_205_2","first-page":"601","volume-title":"Proceedings of the 2018 USENIX Annual Technical Conference (USENIX ATC\u201918)","author":"Lawall Julia","year":"2018","unstructured":"Julia Lawall and Gilles Muller. 2018. Coccinelle: 10 years of automated evolution in the Linux kernel. In Proceedings of the 2018 USENIX Annual Technical Conference (USENIX ATC\u201918). USENIX Association, USA, 601\u2013613. https:\/\/www.usenix.org\/conference\/atc18\/presentation\/lawall"},{"key":"e_1_3_3_206_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/978-3-031-06773-0_4","volume-title":"Proceedings of the 14th International NASA Formal Methods Symposium (NFM\u201922)","volume":"13260","author":"Lawall Julia","year":"2022","unstructured":"Julia Lawall and Gilles Muller. 2022. Automating program transformation with Coccinelle. In Proceedings of the 14th International NASA Formal Methods Symposium (NFM\u201922)(LNCS, Vol. 13260), Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer, Germany, 71\u201387. DOI:10.1007\/978-3-031-06773-0_4"},{"key":"e_1_3_3_207_2","unstructured":"Thierry Lecomte Lilian Burdy and Michael Leuschel. 2020. Formally checking large data sets in the railways. arxiv:1210.6815Proceedings of the Workshop on the Experience of and Advances in Developing Dependable Systems in Event-B (DS-Event-B\u201912)."},{"key":"e_1_3_3_208_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-319-70848-5_6","volume-title":"Proceedings of the 20th Brazilian Symposium on Formal Methods: Foundations and Applications (SBMF\u201917)","volume":"10623","author":"Lecomte Thierry","year":"2017","unstructured":"Thierry Lecomte, David D\u00e9harbe, \u00c9tienne Prun, and Erwan Mottin. 2017. Applying a formal method in industry: A 25-year trajectory. In Proceedings of the 20th Brazilian Symposium on Formal Methods: Foundations and Applications (SBMF\u201917)(LNCS, Vol. 10623), Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.). Springer, Germany, 70\u201387. DOI:10.1007\/978-3-319-70848-5_6"},{"key":"e_1_3_3_209_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"e_1_3_3_210_2","volume-title":"Program Proofs","author":"Leino K. Rustan M.","year":"2023","unstructured":"K. Rustan M. Leino. 2023. Program Proofs. MIT Press, USA. https:\/\/mitpress.mit.edu\/9780262546232\/program-proofs\/"},{"key":"e_1_3_3_211_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2022.111575"},{"key":"e_1_3_3_212_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_3_3_213_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0172-1"},{"key":"e_1_3_3_214_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2017.4041349"},{"key":"e_1_3_3_215_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1993.274940"},{"key":"e_1_3_3_216_2","series-title":"Link\u00f6ping Electronic Press Workshop and Conference Collection","first-page":"36","volume-title":"Proceedings of the 13th MODPROD Workshop 2019: Cyber-Physical Product Development","volume":"21","author":"L\u00f6nn Henrik","year":"2019","unstructured":"Henrik L\u00f6nn. 2019. Model based continuous integration of automotive embedded systems. In Proceedings of the 13th MODPROD Workshop 2019: Cyber-Physical Product Development(Link\u00f6ping Electronic Press Workshop and Conference Collection, Vol. 21). Link\u00f6ping University, Sweden, 36 pages. https:\/\/wcc.ep.liu.se\/index.php\/MODPROD\/article\/view\/116"},{"key":"e_1_3_3_217_2","first-page":"1","volume-title":"Proceedings of the 10th International Symposium on Industrial Embedded Systems (SIES\u201915)","author":"Mahmud Nesredin","year":"2015","unstructured":"Nesredin Mahmud, Cristina Seceleanu, and Oscar Ljungkrantz. 2015. ReSA: An ontology-based requirement specification language tailored to automotive systems. In Proceedings of the 10th International Symposium on Industrial Embedded Systems (SIES\u201915). IEEE, USA, 1\u201310. DOI:10.1109\/SIES.2015.7185035"},{"key":"e_1_3_3_218_2","series-title":"ACSIS","doi-asserted-by":"crossref","first-page":"1737","DOI":"10.15439\/2016F404","volume-title":"Proceedings of the 18th Federated Conference on Computer Science and Information Systems (FedCSIS\u201916)","volume":"8","author":"Mahmud Nesredin","year":"2016","unstructured":"Nesredin Mahmud, Cristina Seceleanu, and Oscar Ljungkrantz. 2016. ReSA tool: Structured requirements specification and SAT-based consistency-checking. In Proceedings of the 18th Federated Conference on Computer Science and Information Systems (FedCSIS\u201916)(ACSIS, Vol. 8), Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki (Eds.). IEEE, USA, 1737\u20131746. DOI:10.15439\/2016F404"},{"key":"e_1_3_3_219_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17581-2_13"},{"key":"e_1_3_3_220_2","unstructured":"Nadja Marko Eike M\u00f6hlmann Dejan Ni\u010dkovi\u0107 J\u00fcrgen Niehaus Peter Priller and Martijn Rooker. 2021. Challenges of Engineering Safe and Secure Highly Automated Vehicles: Whitepaper. arxiv:2103.03544"},{"key":"e_1_3_3_221_2","series-title":"LNCS","first-page":"211","volume-title":"Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918)","volume":"10806","author":"Marsso Lina","year":"2018","unstructured":"Lina Marsso, Radu Mateescu, and Wendelin Serwe. 2018. TESTOR: A modular tool for on-the-fly conformance test case generation. In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918)(LNCS, Vol. 10806), Dirk Beyer and Marieke Huisman (Eds.). Springer, Germany, 211\u2013228. DOI:10.1007\/978-3-319-89963-3_13"},{"key":"e_1_3_3_222_2","series-title":"EPTCS","first-page":"200","volume-title":"Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems (MARS\u201920)","volume":"316","author":"Mateescu Radu","year":"2020","unstructured":"Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin. 2020. Modeling an asynchronous circuit dedicated to the protection against physical attacks. In Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems (MARS\u201920)(EPTCS, Vol. 316), Ansgar Fehnker and Hubert Garavel (Eds.). Open Publishing Association, Australia, 200\u2013239. DOI:10.4204\/EPTCS.316.8"},{"key":"e_1_3_3_223_2","first-page":"112","volume-title":"Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201915)","author":"Mattarei Cristian","year":"2015","unstructured":"Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, and Kristin Y. Rozier. 2015. Comparing different functional allocations in automated air traffic control design. In Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201915), Roope Kaivola and Thomas Wahl (Eds.). IEEE, USA, 112\u2013119. DOI:10.1109\/FMCAD.2015.7542260"},{"key":"e_1_3_3_224_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-018-0488-3"},{"key":"e_1_3_3_225_2","first-page":"1","volume-title":"Proceedings of the 29th IEEE Aerospace Conference (AERO\u201908)","author":"Mehlitz Peter C.","year":"2008","unstructured":"Peter C. Mehlitz. 2008. Trust your model \u2013 verifying aerospace system models with Java\u2122 pathfinder. In Proceedings of the 29th IEEE Aerospace Conference (AERO\u201908). IEEE, USA, 1\u201311. DOI:10.1109\/AERO.2008.4526573"},{"key":"e_1_3_3_226_2","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_3_227_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2008.306"},{"key":"e_1_3_3_228_2","first-page":"25","volume-title":"Proceedings of the 20th High Confidence Software and Systems Conference (HCSS\u201912)","author":"Miller Steven P.","year":"2012","unstructured":"Steven P. Miller. 2012. Lessons from twenty years of industrial formal methods. In Proceedings of the 20th High Confidence Software and Systems Conference (HCSS\u201912). Cyber-Physical Systems Virtual Organization, USA, 25 pages. http:\/\/cps-vo.org\/node\/3434"},{"key":"e_1_3_3_229_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"Milner Robin","year":"1980","unstructured":"Robin Milner. 1980. A Calculus of Communicating Systems. LNCS, Vol. 92. Springer, Germany. DOI:10.1007\/3-540-10235-3"},{"key":"e_1_3_3_230_2","doi-asserted-by":"publisher","DOI":"10.1109\/jproc.1998.658762"},{"key":"e_1_3_3_231_2","volume-title":"Programming from Specifications","author":"Morgan Carroll","year":"1990","unstructured":"Carroll Morgan. 1990. Programming from Specifications. Prentice-Hall, USA."},{"key":"e_1_3_3_232_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_3_3_233_2","series-title":"LNCS","first-page":"337","volume-title":"Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908)","volume":"4963","author":"Moura Leonardo de","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908)(LNCS, Vol. 4963), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, Germany, 337\u2013340. DOI:10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_234_2","series-title":"LNCS","first-page":"625","volume-title":"Proceedings of the 28th International Conference on Automated Deduction (CADE\u201921)","volume":"12699","author":"Moura Leonardo de","year":"2021","unstructured":"Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Proceedings of the 28th International Conference on Automated Deduction (CADE\u201921)(LNCS, Vol. 12699), Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.). Springer, Germany, 625\u2013635. DOI:10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_3_235_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.43"},{"key":"e_1_3_3_236_2","volume-title":"KB3D Reference Manual","author":"Munoz Cesar","year":"2005","unstructured":"Cesar Munoz, Radu Siminiceanu, Victor A. Carreno, and Gilles Dowek. 2005. KB3D Reference Manual. Technical Report NASA\/TM-2005-213769. NASA. https:\/\/ntrs.nasa.gov\/citations\/20050186553"},{"key":"e_1_3_3_237_2","doi-asserted-by":"publisher","DOI":"10.1007\/11916246_16"},{"key":"e_1_3_3_238_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.002"},{"key":"e_1_3_3_239_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0089-2"},{"key":"e_1_3_3_240_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_3_241_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-05156-3"},{"key":"e_1_3_3_242_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel (Eds.). 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer, Germany. DOI:10.1007\/3-540-45949-9"},{"key":"e_1_3_3_243_2","first-page":"6","volume-title":"Proceedings of the 1st Brazilian Workshop on Systematic and Automated Software Testing (SAST\u201907)","author":"Nogueira Sidney","year":"2011","unstructured":"Sidney Nogueira, Emanuela Cartaxo, Dante Torres, Eduardo Aranha, and Rafael Marques. 2011. Model based test generation: An industrial experience. In Proceedings of the 1st Brazilian Workshop on Systematic and Automated Software Testing (SAST\u201907). SBC, Brazil, 6 pages."},{"key":"e_1_3_3_244_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0258-z"},{"key":"e_1_3_3_245_2","first-page":"530","volume-title":"Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS\u201921)","author":"Oberhauser Jonas","year":"2021","unstructured":"Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, and Viktor Vafeiadis. 2021. VSync: Push-button verification and optimization for synchronization primitives on weak memory models. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS\u201921). ACM, USA, 530\u2013545. DOI:10.1145\/3445814.3446748"},{"key":"e_1_3_3_246_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_3_247_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-64021-1"},{"key":"e_1_3_3_248_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-015-0374-1"},{"key":"e_1_3_3_249_2","series-title":"LNCS","first-page":"748","volume-title":"Proceedings of the 11th International Conference on Automated Deduction (CADE\u201992)","volume":"607","author":"Owre Sam","year":"1992","unstructured":"Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: A prototype verification system. In Proceedings of the 11th International Conference on Automated Deduction (CADE\u201992)(LNCS, Vol. 607), Deepak Kapur (Ed.). Springer, Germany, 748\u2013752. DOI:10.1007\/3-540-55602-8_217"},{"key":"e_1_3_3_250_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.22"},{"key":"e_1_3_3_251_2","first-page":"611","volume-title":"Proceedings of the 7th UKSim\/AMSS European Modelling Symposium (EMS\u201913)","author":"Peng Zhaoguang","year":"2013","unstructured":"Zhaoguang Peng, Yu Lu, Alice Miller, Chris W. Johnson, and Tingdi Zhao. 2013. A probabilistic model checking approach to analysing reliability, availability, and maintainability of a single satellite system. In Proceedings of the 7th UKSim\/AMSS European Modelling Symposium (EMS\u201913). IEEE, USA, 611\u2013616. DOI:10.1109\/EMS.2013.102"},{"key":"e_1_3_3_252_2","volume-title":"Copilot 3","author":"Perez Ivan","year":"2020","unstructured":"Ivan Perez, Frank Dedden, and Alwyn Goodloe. 2020. Copilot 3. Technical Report NASA\/TM\u20132020\u2013220587. NASA. https:\/\/ntrs.nasa.gov\/citations\/20200003164"},{"key":"e_1_3_3_253_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2015.03.007"},{"key":"e_1_3_3_254_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/978-3-642-16612-9_26","volume-title":"Proceedings of the 1st International Conference on Runtime Verification (RV\u201910)","volume":"6418","author":"Pike Lee","year":"2010","unstructured":"Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. 2010. Copilot: A hard real-time runtime monitor. In Proceedings of the 1st International Conference on Runtime Verification (RV\u201910)(LNCS, Vol. 6418), Howard Barringer, Yli\u00e8s Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, and Nikolai Tillmann (Eds.). Springer, Germany, 345\u2013359. DOI:10.1007\/978-3-642-16612-9_26"},{"key":"e_1_3_3_255_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_3_256_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR\u201908)","volume":"5195","author":"Platzer Andr\u00e9","year":"2008","unstructured":"Andr\u00e9 Platzer and Jan-David Quesel. 2008. KeYmaera: A hybrid theorem prover for hybrid systems (system description). In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR\u201908)(LNCS, Vol. 5195), Alessandro Armando, Peter Baumgartner, and Gilles Dowek (Eds.). Springer, Germany, 171\u2013178. DOI:10.1007\/978-3-540-71070-7_15"},{"key":"e_1_3_3_257_2","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS\u201977)","author":"Pnueli Amir","year":"1977","unstructured":"Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS\u201977). IEEE, USA, 46\u201357. DOI:10.1109\/SFCS.1977.32"},{"key":"e_1_3_3_258_2","unstructured":"Radio Technical Commission for Aeronautics (RTCA). 1992. DO-178B: Software Considerations in Airborne Systems and Equipment Certification. https:\/\/www.rtca.org\/products\/"},{"key":"e_1_3_3_259_2","unstructured":"Radio Technical Commission for Aeronautics (RTCA). 2000. DO-254: Design Assurance Guidance for Airborne Electronic Hardware. https:\/\/www.rtca.org\/products\/"},{"key":"e_1_3_3_260_2","unstructured":"Radio Technical Commission for Aeronautics (RTCA). 2011. DO-333: Formal Methods Supplement to DO-178C and DO-278A. https:\/\/www.rtca.org\/content\/standards-guidance-materials"},{"key":"e_1_3_3_261_2","unstructured":"Radio Technical Commission for Aeronautics (RTCA). 2012. DO-178C\/ED-12C: Software Considerations in Airborne Systems and Equipment Certification. https:\/\/www.rtca.org\/products\/"},{"key":"e_1_3_3_262_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/978-3-031-60698-4_24","volume-title":"Proceedings of the 16th International NASA Formal Methods Symposium (NFM\u201924)","volume":"14627","author":"Ramnath Sarnath","year":"2024","unstructured":"Sarnath Ramnath and Stephen Walk. 2024. Structuring formal methods into the undergraduate computer science curriculum. In Proceedings of the 16th International NASA Formal Methods Symposium (NFM\u201924)(LNCS, Vol. 14627), Nathaniel Benz, Divya Gopinath, and Nija Shi (Eds.). Springer, Germany, 399\u2013405. DOI:10.1007\/978-3-031-60698-4_24"},{"key":"e_1_3_3_263_2","article-title":"Verification and Validation in VLSI","author":"Rao Goutham","year":"2022","unstructured":"Goutham Rao. 2022. Verification and Validation in VLSI. ChipEdge Technologies. https:\/\/chipedge.com\/verification-and-validation-in-vlsi","journal-title":"ChipEdge Technologies"},{"key":"e_1_3_3_264_2","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-45489-3","volume-title":"Stochastic Model Checking: Advanced Lectures of the International Autumn School on Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems (ROCKS\u201912)","author":"Remke Anne","year":"2014","unstructured":"Anne Remke and Mari\u00eblle Stoelinga (Eds.). 2014. Stochastic Model Checking: Advanced Lectures of the International Autumn School on Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems (ROCKS\u201912). LNCS, Vol. 8453. Springer, Germany. DOI:10.1007\/978-3-662-45489-3"},{"key":"e_1_3_3_265_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-48660-7_26","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE\u201999)","volume":"1632","author":"Riazanov Alexandre","year":"1999","unstructured":"Alexandre Riazanov and Andrei Voronkov. 1999. Vampire. In Proceedings of the 16th International Conference on Automated Deduction (CADE\u201999)(LNCS, Vol. 1632), Harald Ganzinger (Ed.). Springer, Germany, 292\u2013296. DOI:10.1007\/3-540-48660-7_26"},{"key":"e_1_3_3_266_2","volume-title":"Introduction to Static Analysis","author":"Rival Xavier","year":"2020","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis. MIT Press, USA. https:\/\/mitpress.mit.edu\/9780262043410\/introduction-to-static-analysis\/"},{"key":"e_1_3_3_267_2","volume-title":"Handbook of Automated Reasoning","author":"Robinson J. Alan","year":"2001","unstructured":"J. Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier, The Netherlands. https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"key":"e_1_3_3_268_2","first-page":"132","volume-title":"Proceedings of the 11th European Dependable Computing Conference (EDCC\u201915)","author":"Rodriguez Luis R.","year":"2015","unstructured":"Luis R. Rodriguez and Julia Lawall. 2015. Increasing automation in the backporting of Linux drivers using Coccinelle. In Proceedings of the 11th European Dependable Computing Conference (EDCC\u201915). IEEE, USA, 132\u2013143. DOI:10.1109\/EDCC.2015.23"},{"key":"e_1_3_3_269_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-38800-3"},{"key":"e_1_3_3_270_2","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe A. W. (Bill)","year":"1997","unstructured":"A. W. (Bill) Roscoe. 1997. The Theory and Practice of Concurrency. Prentice Hall, USA."},{"key":"e_1_3_3_271_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.06.002"},{"key":"e_1_3_3_272_2","series-title":"LNCS","first-page":"1","volume-title":"Proceedings of the 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE\u201916)","volume":"9971","author":"Rozier Kristin Y.","year":"2016","unstructured":"Kristin Y. Rozier. 2016. Specification: The biggest bottleneck in formal methods and autonomy. In Proceedings of the 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE\u201916)(LNCS, Vol. 9971), Marsha Chechik and Sandrine Blazy (Eds.). Springer, Germany, 1\u201319. DOI:10.1007\/978-3-319-48869-1_2"},{"key":"e_1_3_3_273_2","first-page":"1","volume-title":"Proceedings of the 13th Spring Simulation Conference (SpringSim\u201919)","author":"Rozier Kristin Y.","year":"2019","unstructured":"Kristin Y. Rozier. 2019. From simulation to runtime verification and back: Connecting single-run verification techniques. In Proceedings of the 13th Spring Simulation Conference (SpringSim\u201919). IEEE, USA, 1\u201310. DOI:10.23919\/SpringSim.2019.8732915"},{"key":"e_1_3_3_274_2","series-title":"Kalpa Publications in Computing","doi-asserted-by":"crossref","first-page":"138","DOI":"10.29007\/5pch","volume-title":"Proceedings of the International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES\u201917)","volume":"3","author":"Rozier Kristin Y.","year":"2017","unstructured":"Kristin Y. Rozier and Johann Schumann. 2017. R2U2: Tool overview. In Proceedings of the International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES\u201917)(Kalpa Publications in Computing, Vol. 3), Giles Reger and Klaus Havelund (Eds.). EasyChair, UK, 138\u2013156. DOI:10.29007\/5pch"},{"key":"e_1_3_3_275_2","doi-asserted-by":"publisher","DOI":"10.1016\/0376-5075(78)90016-8"},{"key":"e_1_3_3_276_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-031-13185-1_1","volume-title":"Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922)","volume":"13371","author":"Rungta Neha","year":"2022","unstructured":"Neha Rungta. 2022. A billion SMT queries a day. In Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922)(LNCS, Vol. 13371), Sharon Shoham and Yakir Vizel (Eds.). Springer, Germany, 3\u201318. DOI:10.1007\/978-3-031-13185-1_1"},{"key":"e_1_3_3_277_2","volume-title":"Formal Methods and the Certification of Critical Systems","author":"Rushby John","year":"1993","unstructured":"John Rushby. 1993. Formal Methods and the Certification of Critical Systems. Technical Report SRI-CSL-93-7. Computer Science Laboratory, SRI International. http:\/\/www.csl.sri.com\/papers\/csl-93-7\/"},{"key":"e_1_3_3_278_2","first-page":"598","volume-title":"Proceedings of the 37th International Conference on Software Engineering (ICSE\u201915)","author":"Sadowski Caitlin","year":"2015","unstructured":"Caitlin Sadowski, Jeffrey van Gogh, Ciera Jaspan, Emma S\u00f6derberg, and Collin Winter. 2015. Tricorder: Building a program analysis ecosystem. In Proceedings of the 37th International Conference on Software Engineering (ICSE\u201915). IEEE, USA, 598\u2013608. DOI:10.1109\/ICSE.2015.76"},{"key":"e_1_3_3_279_2","doi-asserted-by":"publisher","unstructured":"SAE International. 2022. Architecture Analysis & Design Language (AADL). DOI:10.4271\/AS5506D","DOI":"10.4271\/AS5506D"},{"key":"e_1_3_3_280_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-031-19762-8_20","volume-title":"Proceedings of the 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Practice (ISoLA\u201922)","volume":"13704","author":"Seisenberger Monika","year":"2022","unstructured":"Monika Seisenberger, Maurice H. ter Beek, Xiuyi Fan, Alessio Ferrari, Anne E. Haxthausen, Phillip James, Andrew Lawrence, Bas Luttik, Jaco van de Pol, and Simon Wimmer. 2022. Safe and secure future AI-driven railway technologies: Challenges for formal methods in railway. In Proceedings of the 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Practice (ISoLA\u201922)(LNCS, Vol. 13704), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, Germany, 246\u2013268. DOI:10.1007\/978-3-031-19762-8_20"},{"key":"e_1_3_3_281_2","first-page":"263","volume-title":"Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE\u201905)","author":"Sen Koushik","year":"2005","unstructured":"Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A concolic unit testing engine for C. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE\u201905). ACM, USA, 263\u2013272. DOI:10.1145\/1081706.1081750"},{"key":"e_1_3_3_282_2","series-title":"LNCS","first-page":"532","volume-title":"Proceedings of the 2nd World Congress on Formal Methods (FM\u201909)","volume":"5850","author":"Souyris Jean","year":"2009","unstructured":"Jean Souyris, Virginie Wiels, David Delmas, and Herv\u00e9 Delseny. 2009. Formal verification of avionics software products. In Proceedings of the 2nd World Congress on Formal Methods (FM\u201909)(LNCS, Vol. 5850), Ana Cavalcanti and Dennis Dams (Eds.). Springer, Germany, 532\u2013546. DOI:10.1007\/978-3-642-05089-3_34"},{"key":"e_1_3_3_283_2","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Understanding Z: A Specification Language and its Formal Semantics","author":"Spivey J. Michael","year":"1988","unstructured":"J. Michael Spivey. 1988. Understanding Z: A Specification Language and its Formal Semantics. Cambridge Tracts in Theoretical Computer Science, Vol. 3. Cambridge University Press, UK."},{"key":"e_1_3_3_284_2","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1109\/CMPASS.1996.507877","volume-title":"Proceedings of 11th Annual Conference on Computer Assurance (COMPASS\u201996)","author":"Sreemani Tirumale","year":"1996","unstructured":"Tirumale Sreemani and Joanne M. Atlee. 1996. Feasibility of model checking software requirements: A case study. In Proceedings of 11th Annual Conference on Computer Assurance (COMPASS\u201996). IEEE, USA, 77\u201388. DOI:10.1109\/CMPASS.1996.507877"},{"key":"e_1_3_3_285_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-024-00746-1"},{"key":"e_1_3_3_286_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-60385-9_2","volume-title":"Proceedings of the 8th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201995)","volume":"987","author":"Stern Ulrich","year":"1995","unstructured":"Ulrich Stern and David L. Dill. 1995. Automatic verification of the SCI cache coherence protocol. In Proceedings of the 8th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u201995)(LNCS, Vol. 987), Paolo Camurati and Hans Eveking (Eds.). Springer, Germany, 21\u201334. DOI:10.1007\/3-540-60385-9_2"},{"key":"e_1_3_3_287_2","volume-title":"Fuzzing: Brute Force Vulnerability Discovery","author":"Sutton Michael","year":"2007","unstructured":"Michael Sutton, Adam Greene, and Pedram Amini. 2007. Fuzzing: Brute Force Vulnerability Discovery. Addison-Wesley, USA."},{"key":"e_1_3_3_288_2","first-page":"9\/1\u20139\/3","volume-title":"Proceedings of the IEE Colloquium on Safety Critical Software in Vehicle and Traffic Control","author":"Thomas Martyn","year":"1990","unstructured":"Martyn Thomas. 1990. The role of formal methods in developing safety-critical software. In Proceedings of the IEE Colloquium on Safety Critical Software in Vehicle and Traffic Control. IET, UK, 9\/1\u20139\/3. DOI:10.1016\/0141-9331(90)90127-H"},{"issue":"1","key":"e_1_3_3_289_2","first-page":"35","article-title":"A proof of incorrectness using LP: The editing problem from the Therac-25","volume":"1","author":"Thomas Muffy","year":"1994","unstructured":"Muffy Thomas. 1994. A proof of incorrectness using LP: The editing problem from the Therac-25. High Integrity Systems 1, 1 (1994), 35\u201349.","journal-title":"High Integrity Systems"},{"issue":"1","key":"e_1_3_3_290_2","first-page":"3","article-title":"The story of the Therac-25 in LOTOS","volume":"1","author":"Thomas Muffy","year":"1994","unstructured":"Muffy Thomas. 1994. The story of the Therac-25 in LOTOS. High Integrity Systems 1, 1 (1994), 3\u201317.","journal-title":"High Integrity Systems"},{"key":"e_1_3_3_291_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68270-9_5"},{"key":"e_1_3_3_292_2","doi-asserted-by":"crossref","DOI":"10.1002\/9781119285441","volume-title":"Probability and Statistics with Reliability, Queuing, and Computer Science Applications","author":"Trivedi Kishor S.","year":"2016","unstructured":"Kishor S. Trivedi. 2016. Probability and Statistics with Reliability, Queuing, and Computer Science Applications. Wiley, UK. https:\/\/www.wiley.com\/en-us\/Probability+and+Statistics+with+Reliability%2C+Queuing%2C+and+Computer+Science+Applications%2C+2nd+Edition-p-x000204691"},{"key":"e_1_3_3_293_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_3_3_294_2","unstructured":"Werner Vogels. 2021. Diving Deep on S3 Consistency. https:\/\/www.allthingsdistributed.com\/2021\/04\/s3-strong-consistency.html"},{"key":"e_1_3_3_295_2","series-title":"LNCS","first-page":"620","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914)","volume":"8413","author":"Essen Christian von","year":"2014","unstructured":"Christian von Essen and Dimitra Giannakopoulou. 2014. Analyzing the next generation airborne collision avoidance system. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914)(LNCS, Vol. 8413), Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer, Germany, 620\u2013635. DOI:10.1007\/978-3-642-54862-8_54"},{"key":"e_1_3_3_296_2","series-title":"LNCS","first-page":"382","volume-title":"Proceedings of the 17th International Conference on Formal Engineering Methods (ICFEM\u201915)","volume":"9407","author":"Wang Shuling","year":"2015","unstructured":"Shuling Wang, Naijun Zhan, and Liang Zou. 2015. An improved HHL prover: An interactive theorem prover for hybrid systems. In Proceedings of the 17th International Conference on Formal Engineering Methods (ICFEM\u201915)(LNCS, Vol. 9407), Michael J. Butler, Sylvain Conchon, and Fatiha Za\u00efdi (Eds.). Springer, Germany, 382\u2013399. DOI:10.1007\/978-3-319-25423-4_25"},{"key":"e_1_3_3_297_2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.224.0393"},{"key":"e_1_3_3_298_2","volume-title":"Back to the Building Blocks: A Path Toward Secure and Measurable Software","author":"House The White","year":"2024","unstructured":"The White House. 2024. Back to the Building Blocks: A Path Toward Secure and Measurable Software. Technical Report. White House Office of the National Cyber Director (ONCD). https:\/\/www.whitehouse.gov\/wp-content\/uploads\/2024\/02\/Final-ONCD-Technical-Report.pdf"},{"key":"e_1_3_3_299_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"e_1_3_3_300_2","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_3_301_2","series-title":"LIPIcs","first-page":"33:1\u201333:21","volume-title":"Proceedings of the 13th International Conference on Interactive Theorem Proving (ITP\u201922)","volume":"237","author":"Zhan Bohua","year":"2022","unstructured":"Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia. 2022. Compositional verification of interacting systems using event monads. In Proceedings of the 13th International Conference on Interactive Theorem Proving (ITP\u201922)(LIPIcs, Vol. 237), June Andronick and Leonardo de Moura (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany, 33:1\u201333:21. DOI:10.4230\/LIPIcs.ITP.2022.33"},{"key":"e_1_3_3_302_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.01.002"},{"key":"e_1_3_3_303_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.04.002"},{"key":"e_1_3_3_304_2","first-page":"690","volume-title":"Proceedings of the 33rd IEEE\/ACM International Conference on Computer-Aided Design (ICCAD\u201914)","author":"Zhao Yang","year":"2014","unstructured":"Yang Zhao and Kristin Y. Rozier. 2014. Probabilistic model checking for comparative analysis of automated air traffic control systems. In Proceedings of the 33rd IEEE\/ACM International Conference on Computer-Aided Design (ICCAD\u201914). IEEE, USA, 690\u2013695. DOI:10.1109\/ICCAD.2014.7001427"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689374","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689374","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:45Z","timestamp":1750291545000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689374"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,26]]},"references-count":303,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3689374"],"URL":"https:\/\/doi.org\/10.1145\/3689374","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,26]]},"assertion":[{"value":"2023-09-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}