{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:08Z","timestamp":1781193728335,"version":"3.54.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_16","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:31:35Z","timestamp":1781191895000},"page":"359-366","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Misguarded Computations: A Pattern of Ineffective Conditional Protection"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7809-536X","authenticated-orcid":false,"given":"Oleksandr","family":"Kolchyn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7499-5895","authenticated-orcid":false,"given":"Daria","family":"Rudenko","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"issue":"10","key":"16_CR1","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"issue":"1","key":"16_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/368937","volume":"37","author":"MH ter Beek","year":"2024","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Formal Aspects Comput. 37(1), 1\u201338 (2024). https:\/\/doi.org\/10.1145\/368937","journal-title":"Formal Aspects Comput."},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Varanasi, S.C., et al.: TRACE: toolkit for requirements analysis, capture, and elicitation. In: Dutle, A., Humphrey, L., Titolo, L. (eds) NASA Formal Methods. NFM 2025. Lecture Notes in Computer Science, vol 15682. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-93706-4_22","DOI":"10.1007\/978-3-031-93706-4_22"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Neider, D., Roy, R.: What is formal verification without specifications? A survey on mining LTL specifications. In: Lecture Notes in Computer Science, vol 15262. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_6","DOI":"10.1007\/978-3-031-75778-5_6"},{"issue":"5","key":"16_CR5","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/MAES.2023.3238378","volume":"38","author":"S Paul","year":"2023","unstructured":"Paul, S., et al.: Formal verification of safety-critical aerospace systems. IEEE Aerosp. Electron. Syst. Mag. 38(5), 72\u201388 (2023). https:\/\/doi.org\/10.1109\/MAES.2023.3238378","journal-title":"IEEE Aerosp. Electron. Syst. Mag."},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Stefanovi\u0107, D., et al.: Static code analysis tools: a systematic literature review. In 31st DAAAM International Symposium On Intelligent Manufacturing And Automation, vol. 31, no. 1, pp. 565\u2013573 (2020). https:\/\/doi.org\/10.2507\/31st.daaam.proceedings.078","DOI":"10.2507\/31st.daaam.proceedings.078"},{"issue":"5","key":"16_CR7","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2008.130","volume":"25","author":"N Ayewah","year":"2008","unstructured":"Ayewah, N., Pugh, W., Hovemeyer, D., Morgenthaler, J.D., Penix, J.: Using static analysis to find bugs. IEEE Softw. 25(5), 22\u201329 (2008). https:\/\/doi.org\/10.1109\/MS.2008.130","journal-title":"IEEE Softw."},{"key":"16_CR8","unstructured":"Brat, G.: IKOS: sound static program analysis. In: NASA V&V Commercial Systems TC-3 Conference and Seminar Series (2022)"},{"key":"16_CR9","unstructured":"Clang: a C Language Family Frontend for LLVM. https:\/\/clang.llvm.org\/"},{"key":"16_CR10","unstructured":"Clang-Tidy Checks. https:\/\/clang.llvm.org\/extra\/clang-tidy\/checks\/list.html"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Hom\u00e8s, B. (2024). Fundamentals of software testing. John Wiley & Sons, Hoboken. https:\/\/doi.org\/10.1002\/9781394298976","DOI":"10.1002\/9781394298976"},{"issue":"5","key":"16_CR12","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1049\/sej.1994.0025","volume":"9","author":"J Chilenski","year":"1994","unstructured":"Chilenski, J., Miller, S.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 9(5), 193\u2013200 (1994). https:\/\/doi.org\/10.1049\/sej.1994.0025","journal-title":"Softw. Eng. J."},{"key":"16_CR13","unstructured":"Hayhurst, K.J., Veerhusen, D.S., Chilenski, J.J., Rierson, L.K.: A Practical Tutorial on Modified Condition\/Decision Coverage (No. L-18088) (2001)"},{"issue":"3","key":"16_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2934672","volume":"25","author":"G Gay","year":"2016","unstructured":"Gay, G., et al.: The effect of program and model structure on the effectiveness of MC\/DC test adequacy coverage. ACM Trans. Softw. Eng. Methodol. (TOSEM) 25(3), 1\u201334 (2016). https:\/\/doi.org\/10.1145\/2934672","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Rapps, S., Weyuker, E.J.: Data flow analysis techniques for test data selection. In: Proceedings of the 6th International Conference on Software Engineering (ICSE \u201982), pp. 272\u2013278. ACM Digital Library (1982): https:\/\/doi.org\/10.5555\/800254.807769","DOI":"10.5555\/800254.807769"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Kolchin, A., Potiyenko, S.: Extending data flow coverage to test constraint refinements. In: ter Beek, M.H., Monahan, R. (eds.) Integrated Formal Methods. Lecture Notes in Computer Science, vol 13274 (2022). https:\/\/doi.org\/10.1007\/978-3-031-07727-2_17","DOI":"10.1007\/978-3-031-07727-2_17"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Kosmatov, N., Prevosto, V., Signoles, J.: Guide to Software Verification with Frama-C. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-55608-","DOI":"10.1007\/978-3-031-55608-"},{"key":"16_CR18","unstructured":"MITRE Corporation. CWE Top 25 Most Dangerous Software Weaknesses\u20142025 (2025). https:\/\/cwe.mitre.org\/top25\/archive\/2025\/2025_cwe_top25.html"},{"issue":"7","key":"16_CR19","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/bs.adcom.2018.10.002","volume":"113","author":"G Yang","year":"2019","unstructured":"Yang, G., Filieri, A., Borges, M., Clun, D., Wen, J.: Advances in symbolic execution. Adv. Comput. 113, 225\u2013287 (2019). https:\/\/doi.org\/10.1016\/bs.adcom.2018.10.002","journal-title":"Adv. Comput."},{"issue":"2\u20133","key":"16_CR21","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1561\/2500000002","volume":"2","author":"J Bertrane","year":"2015","unstructured":"Bertrane, J., et al.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2\u20133), 71\u2013190 (2015). https:\/\/doi.org\/10.1561\/2500000002","journal-title":"Found. Trends Program. Lang."},{"key":"16_CR22","unstructured":"NASA F\u2032 Flight Software Framework, FileUplink.cpp, p-use at line 128, c-use at line 132. https:\/\/github.com\/nasa\/fprime\/blob\/devel\/Svc\/FileUplink\/FileUplink.cpp"},{"key":"16_CR23","unstructured":"NASA F\u2032 Flight Software Framework, StringUtils.cpp, p-use at line 43, c-use at line 56. https:\/\/github.com\/nasa\/fprime\/blob\/devel\/Fw\/Types\/StringUtils.cpp"},{"key":"16_CR24","unstructured":"NASA F\u2032 Flight Software Framework, Directory.cpp, p-use at line 34, c-use at line 35. https:\/\/github.com\/nasa\/fprime\/blob\/devel\/Os\/Posix\/Directory.cpp"},{"key":"16_CR25","unstructured":"NASA Core Flight Executive (cFE), cfe_tbl_task_cmds.c, p-use at line 413, c-use at 423. https:\/\/github.com\/nasa\/cFE\/blob\/main\/modules\/tbl\/fsw\/src\/cfe_tbl_task_cmds.c"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:31:39Z","timestamp":1781191899000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}