{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:49:52Z","timestamp":1761677392139,"version":"build-2065373602"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2025,10]]},"DOI":"10.1007\/s10009-025-00828-8","type":"journal-article","created":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:05:02Z","timestamp":1761559502000},"page":"487-510","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Logika: the Sireum verification framework"],"prefix":"10.1007","volume":"27","author":[{"family":"Robby","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason","family":"Belt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,27]]},"reference":[{"key":"828_CR1","series-title":"LNCS","volume-title":"Deductive Software Verification - the KeY Book - from Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - the KeY Book - from Theory to Practice. LNCS, vol.\u00a010001. Springer, Berlin (2016)"},{"key":"828_CR2","first-page":"1","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"J. Backes","year":"2018","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using SMT. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a01\u20139. IEEE Press, New York (2018)"},{"key":"828_CR3","first-page":"415","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Barbosa","year":"2022","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., et al.: cvc5: a versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0415\u2013442. Springer, Berlin (2022)"},{"issue":"10","key":"828_CR4","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H. Barbosa","year":"2023","unstructured":"Barbosa, H., Barrett, C.W., Cook, B., Dutertre, B., Kremer, G., Lachnitt, H., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Tinelli, C., Zohar, Y.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023)","journal-title":"Commun. ACM"},{"key":"828_CR5","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1109\/TSE.2010.39","volume":"37","author":"L. Baresi","year":"2011","unstructured":"Baresi, L., Ghezzi, C., Mottola, L.: Loupe: verifying publish-subscribe architectures with a magnifying lens. IEEE Trans. Softw. Eng. 37, 228\u2013246 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"828_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects (FMCO 2005)","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects (FMCO 2005). Lecture Notes in Computer Science, vol.\u00a04111, pp.\u00a0364\u2013387. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"828_CR7","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"International Conference on Computer Aided Verification (CAV)","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: International Conference on Computer Aided Verification (CAV), pp.\u00a0171\u2013177. Springer, Berlin (2011)"},{"key":"828_CR8","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/978-3-642-20398-5_6","volume-title":"NASA Formal Methods","author":"J. Belt","year":"2011","unstructured":"Belt, J., Hatcliff, J., Robby, Chalin, P., Hardin, D., Deng, X.: Bakar kiasan: flexible contract checking for critical systems using symbolic execution. In: NASA Formal Methods, pp.\u00a058\u201372 (2011)"},{"key":"828_CR9","doi-asserted-by":"crossref","unstructured":"Belt, J., Hatcliff, J., Robby, S.J., Carciofini, J., Carpenter, T., Mercer, E., Amundson, I., Babar, J., Cofer, D., Hardin, D., Hoech, K., Slind, K., Kuz, I., Mcleod, K.: Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Archit. (2022)","DOI":"10.1016\/j.sysarc.2022.102789"},{"key":"828_CR10","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Berlin (2013)"},{"key":"828_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"Software Engineering and Formal Methods (SEFM 2014)","author":"S.J. Blom","year":"2014","unstructured":"Blom, S.J., Huisman, M., van de Pol, J.: The vercors tool for verification of concurrent programs. In: Gnesi, S., Ponse, A.L., de Roever, W.P. (eds.) Software Engineering and Formal Methods (SEFM 2014). Lecture Notes in Computer Science, vol.\u00a08368, pp.\u00a0150\u2013165. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_9"},{"key":"828_CR12","series-title":"LNCS","first-page":"1","volume-title":"10th International Conference on Automated Deduction (CADE)","author":"R.S. Boyer","year":"1990","unstructured":"Boyer, R.S., Moore, J.S.: A theorem prover for a computational logic. In: 10th International Conference on Automated Deduction (CADE). LNCS, vol.\u00a0449, pp.\u00a01\u201315. Springer, Berlin (1990)"},{"issue":"3","key":"828_CR13","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7(3), 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"828_CR14","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1145\/255471.255563","volume-title":"Proceedings of the Conference on TRI-ADA\u201990","author":"B. Carr\u00e9","year":"1990","unstructured":"Carr\u00e9, B., Garnsworthy, J.: Spark\u2014an annotated ada subset for safety-critical programming. In: Proceedings of the Conference on TRI-ADA\u201990, pp.\u00a0392\u2013402 (1990)"},{"issue":"3","key":"828_CR15","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/MSEC.2022.3151733","volume":"20","author":"D.D. Cofer","year":"2022","unstructured":"Cofer, D.D., Amundson, I., Babar, J., Hardin, D.S., Slind, K., Alexander, P., Hatcliff, J., Robby, K.G., Lewis, C., Mercer, E., Shackleton, J.: Cyberassured systems engineering at scale. IEEE Secur. Priv. 20(3), 52\u201364 (2022)","journal-title":"IEEE Secur. Priv."},{"key":"828_CR16","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1145\/337180.337234","volume-title":"Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000)","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby, R.C., Stoller, M.B., Wallentine, T.: Bandera: a source-level interface for model checking Java programs. In: Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), pp.\u00a0762\u2013765. ACM, Limerick (2000). https:\/\/doi.org\/10.1145\/337180.337234"},{"key":"828_CR17","unstructured":"cvc5 performance regression GitHub issues. https:\/\/github.com\/cvc5\/cvc5\/issues\/8736"},{"key":"828_CR18","series-title":"LNCS","first-page":"625","volume-title":"28th International Conference on Automated Deduction (CADE)","author":"L. de Moura","year":"2021","unstructured":"de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: 28th International Conference on Automated Deduction (CADE). LNCS, vol.\u00a012699, pp.\u00a0625\u2013635. Springer, Berlin (2021)"},{"key":"828_CR19","first-page":"137","volume-title":"Leveraging Applications of Formal Methods, Second International Symposium, ISoLA 2006","author":"X. Deng","year":"2006","unstructured":"Deng, X., Robby, Hatcliff, J.: Kiasan: a verification and test-case generation framework for Java based on symbolic execution. In: Leveraging Applications of Formal Methods, Second International Symposium, ISoLA 2006, Paphos, Cyprus, 15\u201319 November 2006, p.\u00a0137 (2006)"},{"key":"828_CR20","volume-title":"Testing: Academic and Industrial Conference Practice and Research Techniques (TAICPART 2007)","author":"X. Deng","year":"2007","unstructured":"Deng, X., Robby, Hatcliff, J.: Kiasan\/kunit: Automatic test case generation and analysis feedback for open object-oriented systems. In: Testing: Academic and Industrial Conference Practice and Research Techniques (TAICPART 2007) (2007)"},{"issue":"3","key":"828_CR21","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s10515-011-0089-9","volume":"19","author":"X. Deng","year":"2012","unstructured":"Deng, X., Lee, J., Robby: Efficient and formal generalized symbolic execution. Autom. Softw. Eng. 19(3), 233\u2013301 (2012)","journal-title":"Autom. Softw. Eng."},{"key":"828_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1007\/978-3-319-48869-1_5","volume-title":"8th International Conference on Verified Software, Theories, Tools, and Experiments (VSTTE)","author":"R. Dockins","year":"2016","unstructured":"Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing semantic models of programs with the software analysis workbench. In: 8th International Conference on Verified Software, Theories, Tools, and Experiments (VSTTE). LNCS, vol.\u00a09971, pp.\u00a056\u201372 (2016)"},{"key":"828_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-540-45212-6_12","volume-title":"3rd International Conference on Embedded Software (EMSOFT)","author":"M.B. Dwyer","year":"2003","unstructured":"Dwyer, M.B., Robby, D.X., Hatcliff, J.: Space reductions for model checking quasi-cyclic systems. In: 3rd International Conference on Embedded Software (EMSOFT). Lecture Notes in Computer Science, vol.\u00a02855, pp.\u00a0173\u2013189. Springer, Berlin (2003)"},{"key":"828_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Proceedings of the 22nd European Symposium on Programming (ESOP 2013)","author":"J.C. Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Dam, M. (ed.) Proceedings of the 22nd European Symposium on Programming (ESOP 2013). Lecture Notes in Computer Science, vol.\u00a07792, pp.\u00a01\u201316. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"828_CR25","unstructured":"Galois\u2019 HARDENS repository. https:\/\/github.com\/GaloisInc\/HARDENS"},{"key":"828_CR26","series-title":"LNCS","first-page":"45","volume-title":"19th International Conference on Formal Aspects of Component Software (FACS)","author":"S. Hallerstede","year":"2023","unstructured":"Hallerstede, S., Hatcliff, J.: A mechanized semantics for component-based systems in the HAMR AADL runtime. In: 19th International Conference on Formal Aspects of Component Software (FACS). LNCS, vol.\u00a014485, pp.\u00a045\u201364. Springer, Berlin (2023)"},{"key":"828_CR27","volume-title":"Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST\u201925)","author":"S. Hallerstede","year":"2025","unstructured":"Hallerstede, S., Robby, H.J.: Danvy\u2019s mystery functions in Slang. In: Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST\u201925) (2025)"},{"key":"828_CR28","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/978-3-031-71379-8_7","volume-title":"6th Formal Methods Teaching Workshop (FMTea)","author":"S. Hallerstede","year":"2024","unstructured":"Hallerstede, S., Hatcliff, J., Robby: Teaching with logika: conceiving and constructing correct software. In: 6th Formal Methods Teaching Workshop (FMTea). LNCS, vol.\u00a014939, pp.\u00a0106\u2013123. Springer, Berlin (2024)"},{"key":"828_CR29","first-page":"39","volume-title":"Proceedings of the 2025 International Conference on Formal Methods for Industrial Critical Systems (FMICS 2025)","author":"S. Hallerstede","year":"2026","unstructured":"Hallerstede, S., Robby, H.J., Belt, J., Hardin, D.: Proof engineering in Logika: synergistically integrating automated and semi-automated program verification. In: Proceedings of the 2025 International Conference on Formal Methods for Industrial Critical Systems (FMICS 2025), pp.\u00a039\u201358 (2026)"},{"key":"828_CR30","first-page":"61","volume-title":"ACL2 Theorem Prover and Its Applications (ACL2-2018), EPTCS","author":"D. Hardin","year":"2018","unstructured":"Hardin, D., Slind, K.: Using ACL2 in the design of efficient, verifiable data structures for high-assurance systems. In: ACL2 Theorem Prover and Its Applications (ACL2-2018), EPTCS, vol.\u00a0280, pp.\u00a061\u201376 (2018)"},{"key":"828_CR31","unstructured":"Hatcliff, J.: Course material for High Assurance Systems. http:\/\/s21.highassurance.santoslab.org\/lectures.html (2024)"},{"key":"828_CR32","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-031-73887-6_9","volume-title":"The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering","author":"J. Hatcliff","year":"2025","unstructured":"Hatcliff, J., Belt, J.: The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering pp.\u00a093\u2013117. Springer, Switzerland (2025). https:\/\/doi.org\/10.1007\/978-3-031-73887-6_9"},{"key":"828_CR33","first-page":"222","volume-title":"35th International Conference on Software Engineering (ICSE)","author":"J. Hatcliff","year":"2013","unstructured":"Hatcliff, J., Robby, Chalin, P., Belt, J.: Explicating symbolic execution (xSymExe): an evidence-based verification framework. In: 35th International Conference on Software Engineering (ICSE), pp.\u00a0222\u2013231. IEEE Comput. Soc., Los Alamitos (2013)"},{"key":"828_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/978-3-030-89159-6_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)","author":"J. Hatcliff","year":"2021","unstructured":"Hatcliff, J., Belt, J., Robby, C.T.: HAMR: an AADL multi-platform code generation toolset. In: Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). LNCS, vol.\u00a013036, pp.\u00a0274\u2013295 (2021)"},{"key":"828_CR35","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation - 11th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022","author":"J. Hatcliff","year":"2022","unstructured":"Hatcliff, J., Hugues, J., Stewart, D., Wrage, L.: Formalization of the AADL run-time services. In: Leveraging Applications of Formal Methods, Verification and Validation - 11th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022, Rhodes, Greece (2022)"},{"key":"828_CR36","volume-title":"Proceedings of the 2022 ACM Workshop on High Integrity Language Technology, HILT\u201922","author":"J. Hatcliff","year":"2022","unstructured":"Hatcliff, J., Stewart, D., Belt, J., Robby, S.A.: An AADL contract language supporting integrated model- and code-level verification. In: Proceedings of the 2022 ACM Workshop on High Integrity Language Technology, HILT\u201922 (2022)"},{"key":"828_CR37","volume-title":"Formal Methods for Industrial Critical Systems","author":"J. Hatcliff","year":"2023","unstructured":"Hatcliff, J., Belt, J., Robby, L.J., Stewart, D., Carpenter, T.: Automated property-based testing from aadl component contracts. In: Cimatti, A., Titolo, L. (eds.) Formal Methods for Industrial Critical Systems (2023)"},{"key":"828_CR38","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/978-3-031-60698-4_25","volume-title":"16th NASA Formal Methods Symposium (NFM)","author":"J. Hatcliff","year":"2024","unstructured":"Hatcliff, J., Belt, J., Robby, H.D.: Integrated contract-based unit and system testing for component-based systems. In: 16th NASA Formal Methods Symposium (NFM). LNCS, pp.\u00a0406\u2013426. Springer, Berlin (2024)"},{"key":"828_CR39","first-page":"241","volume-title":"Proceedings of the 2025 International Conference on Formal Methods for Industrial Critical Systems (FMICS 2025)","author":"J. Hatcliff","year":"2026","unstructured":"Hatcliff, J., Belt, J., Robby, M.C., Liang, C.: End-to-end formal methods integrated development with SysMLv2 using HAMR. In: Proceedings of the 2025 International Conference on Formal Methods for Industrial Critical Systems (FMICS 2025), pp.\u00a0241\u2013260 (2026)"},{"key":"828_CR40","doi-asserted-by":"crossref","unstructured":"Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: SPARK 2014 and GNATprove. Int. J. Softw. Tools Technol. Transf. 17(6) (2015)","DOI":"10.1007\/s10009-014-0322-5"},{"key":"828_CR41","unstructured":"How we built Cedar with automated reasoning and differential testing. https:\/\/www.amazon.science\/blog\/how-we-built-cedar-with-automated-reasoning-and-differential-testing (2023)"},{"key":"828_CR42","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/2402676.2402680","volume-title":"Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT\u201912","author":"J. Kanig","year":"2012","unstructured":"Kanig, J.: Leading-edge ada verification technologies: combining testing and verification with gnattest and gnatprove - the hi-lite project. In: Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT\u201912, Boston, Massachusetts, USA, December 2-6, 2012, pp.\u00a05\u20136. ACM, New York (2012)"},{"issue":"7","key":"828_CR43","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"OOPSLA1","key":"828_CR44","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1145\/3586037","volume":"7","author":"A. Lattuada","year":"2023","unstructured":"Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA1), 286\u2013315 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"828_CR45","volume-title":"Program Proofs","author":"K.R.M. Leino","year":"2023","unstructured":"Leino, K.R.M.: Program Proofs. MIT Press, Cambridge (2023)"},{"key":"828_CR46","unstructured":"Lempia, D., Miller, S.: DOT\/FAA\/AR-08\/32. Requirements engineering management handbook. Federal Aviation Administration (2009)"},{"key":"828_CR47","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress","author":"X. Leroy","year":"2016","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., Ferdinand, C.: Compcert-a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress (2016)"},{"key":"828_CR48","unstructured":"Logika overview case studies repository. https:\/\/github.com\/santoslab\/logika-overview-case-studies"},{"key":"828_CR49","unstructured":"Logika presentation at the 2022 Trusted Computing Center of Excellence Summit (TCCoE). https:\/\/doc.sireum.org\/venues\/presentations\/logika\/tccoe22\/ (massive parallelization demo from an iPad starts at 22:33)"},{"key":"828_CR50","first-page":"337","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"L.d. Moura","year":"2008","unstructured":"Moura, L.d., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.\u00a0337\u2013340. Springer, Berlin (2008)"},{"key":"828_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)","author":"P. M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Etessami, K. (eds.) Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016). Lecture Notes in Computer Science, vol.\u00a09583, pp.\u00a041\u201362. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"828_CR52","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol.\u00a02283. Springer, Berlin (2002)"},{"key":"828_CR53","series-title":"LNCS","first-page":"748","volume-title":"11th International Conference on Automated Deduction (CADE)","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). LNCS, vol.\u00a0607, pp.\u00a0748\u2013752. Springer, Berlin (1992)"},{"key":"828_CR54","first-page":"267","volume-title":"11th ACM SIGSOFT Symposium on Foundations of Software Engineering Held Jointly with 9th European Software Engineering Conference (ESEC\/FSE)","author":"D.M.B. Robby","year":"2003","unstructured":"Robby, D.M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Held Jointly with 9th European Software Engineering Conference (ESEC\/FSE), pp.\u00a0267\u2013276. ACM, New York (2003)"},{"key":"828_CR55","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/978-3-030-89159-6_17","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)","author":"Robby","year":"2021","unstructured":"Robby, Hatcliff, J.: Slang: the sireum programming language. In: Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pp.\u00a0253\u2013273. Springer, Berlin (2021)"},{"key":"828_CR56","series-title":"LNCS","first-page":"97","volume-title":"29th International Conference on Formal Methods for Industrial Critical Systems (FMICS)","author":"Robby","year":"2024","unstructured":"Robby, Hatcliff, J., Belt, J.: Logika: the sireum verification framework. In: 29th International Conference on Formal Methods for Industrial Critical Systems (FMICS). LNCS, vol.\u00a014952, pp.\u00a097\u2013116. Springer, Berlin (2024)"},{"key":"828_CR57","unstructured":"Sireum website. https:\/\/sireum.org\/"},{"key":"828_CR58","unstructured":"SMT-LIB website. https:\/\/smtlib.cs.uiowa.edu\/"},{"key":"828_CR59","unstructured":"Society of Automotive Engineers: Architecture analysis & design language (AADL): Aerospace Standard AS5506 (2004)"},{"key":"828_CR60","unstructured":"SysML v2 website. https:\/\/www.omgsysml.org\/SysML-2.htm"},{"issue":"4","key":"828_CR61","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/s11334-021-00410-w","volume":"18","author":"H. Thiagarajan","year":"2022","unstructured":"Thiagarajan, H., Hatcliff, J., Robby: Awas: AADL information flow and error propagation analysis framework. Innov. Syst. Softw. Eng. 18(4), 485\u2013504 (2022)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"828_CR62","unstructured":"Thorton, J.: Logical foundations of programming (online textbook for ksu cs 301). https:\/\/textbooks.cs.ksu.edu\/cis301\/index.html"},{"key":"828_CR63","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-66197-1_2","volume-title":"15th International Conference Software Engineering and Formal Methods (SEFM)","author":"Z. Zhang","year":"2017","unstructured":"Zhang, Z., Robby, Hatcliff, J., Moy, Y., Courtieu, P.: Focused certification of an industrial compilation and static verification toolchain. In: 15th International Conference Software Engineering and Formal Methods (SEFM). LNCS, vol.\u00a010469, pp.\u00a017\u201334. Springer, Berlin (2017)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00828-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-025-00828-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00828-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T15:40:22Z","timestamp":1761666022000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-025-00828-8"}},"subtitle":["An overview"],"short-title":[],"issued":{"date-parts":[[2025,10]]},"references-count":63,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["828"],"URL":"https:\/\/doi.org\/10.1007\/s10009-025-00828-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2025,10]]},"assertion":[{"value":"7 October 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 October 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}