{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T02:21:13Z","timestamp":1768357273548,"version":"3.49.0"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","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-15700-3_8","type":"book-chapter","created":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T12:30:14Z","timestamp":1768307414000},"page":"147-172","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Forward Symbolic Execution for\u00a0Trustworthy Automation of\u00a0Binary Code Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5311-1781","authenticated-orcid":false,"given":"Andreas","family":"Lindner","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0228-1240","authenticated-orcid":false,"given":"Karl","family":"Palmskog","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6793-0451","authenticated-orcid":false,"given":"Scott","family":"Constable","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5432-6442","authenticated-orcid":false,"given":"Mads","family":"Dam","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8069-6495","authenticated-orcid":false,"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9251-3679","authenticated-orcid":false,"given":"Hamed","family":"Nemati","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"8_CR1","unstructured":"aiT Worst-Case Execution Time Analyzers. https:\/\/www.absint.com\/ait\/index.htm. Accessed 23 Dec 2022"},{"key":"8_CR2","unstructured":"Cortex-M0 Technical Reference Manual r0p0 - Instruction set summary. https:\/\/developer.arm.com\/documentation\/ddi0432\/c\/programmers-model\/instruction-set-summary. Accessed 23 Dec 2022"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Abella, J., et al.: WCET analysis methods: pitfalls and challenges on their trustworthiness. In: International Symposium on Industrial Embedded Systems, pp. 1\u201310 (2015). https:\/\/doi.org\/10.1109\/SIES.2015.7185039","DOI":"10.1109\/SIES.2015.7185039"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Avgerinos, T., Rebert, A., Cha, S.K., Brumley, D.: Enhancing symbolic execution with Veritesting. In: International Conference on Software Engineering, pp. 1083\u20131094 (2014). https:\/\/doi.org\/10.1145\/2568225.2568293","DOI":"10.1145\/2568225.2568293"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Baldoni, R., Coppa, E., D\u2019elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3) (2018). https:\/\/doi.org\/10.1145\/3182657","DOI":"10.1145\/3182657"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Workshop on Program Analysis for Software Tools and Engineering, pp. 82\u2014-87 (2005). https:\/\/doi.org\/10.1145\/1108792.1108813","DOI":"10.1145\/1108792.1108813"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 112\u2013126. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11679219_9"},{"key":"8_CR8","unstructured":"Bernstein, D.J.: Chacha, a variant of Salsa20. In: Workshop Record of SASC, vol. 8. pp.\u00a03\u20135 (2008). http:\/\/cr.yp.to\/chacha\/chacha-20080128.pdf"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Kiefer, F., Strub, P.Y.: hacspec: Towards verifiable crypto standards. In: International Conference of Security Standardisation Research, pp. 1\u201320 (2018). https:\/\/doi.org\/10.1007\/978-3-030-04762-7_1","DOI":"10.1007\/978-3-030-04762-7_1"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-22110-1_37","volume-title":"Computer Aided Verification","author":"D Brumley","year":"2011","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: a binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 463\u2013469. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_37"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Buiras, P., Nemati, H., Lindner, A., Guanciale, R.: Validation of side-channel models via observation refinement. In: International Symposium on Microarchitecture, pp. 578\u2013591 (2021). https:\/\/doi.org\/10.1145\/3466752.3480130","DOI":"10.1145\/3466752.3480130"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Byhlin, S., Ermedahl, A., Gustafsson, J., Lisper, B.: Applying static WCET analysis to automotive communication software. In: Euromicro Conference on Real-Time Systems, pp. 249\u2013258 (2005). https:\/\/doi.org\/10.1109\/ECRTS.2005.7","DOI":"10.1109\/ECRTS.2005.7"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Cha, S.K., Avgerinos, T., Rebert, A., Brumley, D.: Unleashing mayhem on binary code. In: Symposium on Security and Privacy, pp. 380\u2013394 (2012). https:\/\/doi.org\/10.1109\/SP.2012.31","DOI":"10.1109\/SP.2012.31"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Coen-Porisini, A., Denaro, G., Ghezzi, C., Pezz\u00e9, M.: Using symbolic execution for verifying safety-critical systems. In: European Software Engineering Conference, pp. 142\u2013151 (2001). https:\/\/doi.org\/10.1145\/503209.503230","DOI":"10.1145\/503209.503230"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Cousot, P.: Abstract interpretation. ACM Comput. Surv. 28(2), 324\u2013328 (1996). https:\/\/doi.org\/10.1145\/234528.234740","DOI":"10.1145\/234528.234740"},{"issue":"1","key":"8_CR16","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10766-005-0004-8","volume":"34","author":"D Currie","year":"2006","unstructured":"Currie, D., Feng, X., Fujita, M., Hu, A.J., Kwan, M., Rajan, S.: Embedded software verification using symbolic execution and uninterpreted functions. Int. J. Parallel Prog. 34(1), 61\u201391 (2006). https:\/\/doi.org\/10.1007\/s10766-005-0004-8","journal-title":"Int. J. Parallel Prog."},{"key":"8_CR17","unstructured":"Dahl, O.J., Dijkstra, E.W., Hoare, C.A.R. (eds.): Structured programming. Academic Press Ltd. (1972)"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Daniel, L.A., Bardin, S., Rezk, T.: Binsec\/Rel: efficient relational symbolic execution for constant-time at binary-level. In: Symposium on Security and Privacy, pp. 1021\u20131038 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00074","DOI":"10.1109\/SP40000.2020.00074"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Daniel, L.A., Bardin, S., Rezk, T.: Hunting the Haunter\u2013efficient relational symbolic execution for Spectre with Haunted RelSE. In: Network and Distributed Systems Security (2021). https:\/\/doi.org\/10.14722\/ndss.2021.24286","DOI":"10.14722\/ndss.2021.24286"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Dannenberg, R., Ernst, G.: Formal program verification using symbolic execution. IEEE Trans. Softw. Eng. SE-8(1), 43\u201352 (1982). https:\/\/doi.org\/10.1109\/TSE.1982.234773","DOI":"10.1109\/TSE.1982.234773"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Dasgupta, S., Dinesh, S., Venkatesh, D., Adve, V.S., Fletcher, C.W.: Scalable validation of binary lifters. In: Conference on Programming Language Design and Implementation, pp. 655\u2013671 (2020). https:\/\/doi.org\/10.1145\/3385412.3385964","DOI":"10.1145\/3385412.3385964"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"David, R., et al.: Specification of concretization and symbolization policies in symbolic execution. In: International Symposium on Software Testing and Analysis, pp. 36\u201346 (2016). https:\/\/doi.org\/10.1145\/2931037.2931048","DOI":"10.1145\/2931037.2931048"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Farinier, B., David, R., Bardin, S., Lemerre, M.: Arrays made simpler: an efficient, scalable and thorough preprocessing. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.\u00a057, pp. 363\u2013380 (2018). https:\/\/doi.org\/10.29007\/dc9b","DOI":"10.29007\/dc9b"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-22102-1_12","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2015","unstructured":"Fox, A.: Improved tool support for machine-code decompilation in HOL4. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 187\u2013202. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_12"},{"key":"8_CR26","unstructured":"Fox, A.: L3: A Specification Language for Instruction Set Architectures. https:\/\/acjf3.github.io\/l3. Accessed 17 Nov 2025"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Conference on Programming Language Design and Implementation, pp. 213\u2013223 (2005). https:\/\/doi.org\/10.1145\/1065010.1065036","DOI":"10.1145\/1065010.1065036"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Hamming, R.R.: Art of Doing Science and Engineering: Learning to Learn. CRC Press, Boca Raton (1997). https:\/\/doi.org\/10.1201\/9781482283198","DOI":"10.1201\/9781482283198"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Hansen, T., Schachte, P., S\u00f8ndergaard, H.: State joining and splitting for the symbolic execution of binaries. In: International Workshop on Runtime Verification, pp. 76\u201392 (2009). https:\/\/doi.org\/10.1007\/978-3-642-04694-0_6","DOI":"10.1007\/978-3-642-04694-0_6"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv. 8(3), 331\u2013353 (1976). https:\/\/doi.org\/10.1145\/356674.356677","DOI":"10.1145\/356674.356677"},{"issue":"7","key":"8_CR31","doi-asserted-by":"publisher","first-page":"1038","DOI":"10.1109\/JPROC.2003.814618","volume":"91","author":"R Heckmann","year":"2003","unstructured":"Heckmann, R., Langenbach, M., Thesing, S., Wilhelm, R.: The influence of processor architecture on the design and the results of WCET tools. Proc. IEEE 91(7), 1038\u20131054 (2003). https:\/\/doi.org\/10.1109\/JPROC.2003.814618","journal-title":"Proc. IEEE"},{"key":"8_CR32","unstructured":"HOL development team: HOL interactive theorem prover. https:\/\/hol-theorem-prover.org. Accesed 17 Nov 2025"},{"key":"8_CR33","unstructured":"HolBA contributors: HolBA - Binary analysis in HOL. https:\/\/github.com\/kth-step\/HolBA. Accessed 17 Nov 2025"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Iosif-Lazar, A.F., Al-Sibahi, A.S., Dimovski, A.S., Savolainen, J.E., Sierszecki, K., Wasowski, A.: Experiences from designing and validating a software modernization transformation. In: International Conference on Automated Software Engineering, pp. 597\u2013607 (2015). https:\/\/doi.org\/10.1109\/ASE.2015.84","DOI":"10.1109\/ASE.2015.84"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758\u2013766. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_61"},{"key":"8_CR36","unstructured":"Karlsson, H.A.: S3K: Capability based separation kernel for embedded RISC-V. https:\/\/github.com\/kth-step\/s3k. Accessed 16 Nov 2025"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Kinder, J., Zuleger, F., Veith, H.: An abstract interpretation-based framework for control flow reconstruction from binaries. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 214\u2013228 (2009). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_19","DOI":"10.1007\/978-3-540-93900-9_19"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Kirner, R., Puschner, P.: Classification of WCET analysis techniques. In: International Symposium on Object-Oriented Real-Time Distributed Computing, pp. 190\u2013199 (2005). https:\/\/doi.org\/10.1109\/ISORC.2005.19","DOI":"10.1109\/ISORC.2005.19"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: Conference on Programming Language Design and Implementation, pp. 193\u2013204 (2012). https:\/\/doi.org\/10.1145\/2254064.2254088","DOI":"10.1145\/2254064.2254088"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Li, X., Roychoudhury, A., Mitra, T.: Modeling out-of-order processors for WCET analysis. Real-Time Syst. 34(3), 195\u2013227 (2006). https:\/\/doi.org\/10.1007\/s11241-006-9205-5","DOI":"10.1007\/s11241-006-9205-5"},{"key":"8_CR42","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.scico.2019.01.001","volume":"174","author":"A Lindner","year":"2019","unstructured":"Lindner, A., Guanciale, R., Metere, R.: TrABin: trustworthy analyses of binaries. Sci. Comput. Program. 174, 72\u201389 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.01.001","journal-title":"Sci. Comput. Program."},{"key":"8_CR43","doi-asserted-by":"publisher","unstructured":"Lindner, A., Palmskog, K., Lundberg, D.: HolBA-SE (2025). https:\/\/doi.org\/10.5281\/zenodo.15043917","DOI":"10.5281\/zenodo.15043917"},{"key":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-030-58768-0_11","volume-title":"Software Engineering and Formal Methods","author":"D Lundberg","year":"2020","unstructured":"Lundberg, D., Guanciale, R., Lindner, A., Dam, M.: Hoare-style logic for unstructured programs. In: de Boer, F., Cerone, A. (eds.) SEFM 2020. LNCS, vol. 12310, pp. 193\u2013213. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_11"},{"key":"8_CR45","doi-asserted-by":"publisher","unstructured":"Maroneze, A., Blazy, S., Pichardie, D., Puaut, I.: A formally verified WCET estimation tool. In: International Workshop on Worst-Case Execution Time Analysis, vol.\u00a039, pp. 11\u201320 (2014). https:\/\/doi.org\/10.4230\/OASIcs.WCET.2014.11","DOI":"10.4230\/OASIcs.WCET.2014.11"},{"key":"8_CR46","doi-asserted-by":"publisher","unstructured":"Mazzucato, D., et al.: Relational Hoare logic for realistically modelled machine code. In: Computer Aided Verification, pp. 389\u2013413 (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_19","DOI":"10.1007\/978-3-031-98668-0_19"},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-030-53288-8_12","volume-title":"Computer Aided Verification","author":"H Nemati","year":"2020","unstructured":"Nemati, H., Buiras, P., Lindner, A., Guanciale, R., Jacobs, S.: Validation of abstract side-channel models for computer architectures. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 225\u2013248. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_12"},{"key":"8_CR48","doi-asserted-by":"publisher","unstructured":"Nir, Y., Langley, A.: ChaCha20 and Poly1305 for IETF Protocols. RFC 8439 (2018). https:\/\/doi.org\/10.17487\/RFC8439","DOI":"10.17487\/RFC8439"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"Nowotsch, J., Paulitsch, M.: Leveraging multi-core computing architectures in avionics. In: European Dependable Computing Conference, pp. 132\u2013143 (2012). https:\/\/doi.org\/10.1109\/EDCC.2012.27","DOI":"10.1109\/EDCC.2012.27"},{"issue":"4","key":"8_CR50","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"CS P\u0103s\u0103reanu","year":"2009","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transfer 11(4), 339\u2013353 (2009). https:\/\/doi.org\/10.1007\/s10009-009-0118-1","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Sammler, M., et al.: Islaris: verification of machine code against authoritative ISA semantics. In: International Conference on Programming Language Design and Implementation, pp. 825\u2013840 (2022). https:\/\/doi.org\/10.1145\/3519939.3523434","DOI":"10.1145\/3519939.3523434"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"Saxena, P., Poosankam, P., McCamant, S., Song, D.: Loop-extended symbolic execution on binary programs. In: International Symposium on Software Testing and Analysis, pp. 225\u2013236 (2009). https:\/\/doi.org\/10.1145\/1572272.1572299","DOI":"10.1145\/1572272.1572299"},{"key":"8_CR53","doi-asserted-by":"publisher","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: Conference on Programming Language Design and Implementation, pp. 471\u2013482 (2013). https:\/\/doi.org\/10.1145\/2491956.2462183","DOI":"10.1145\/2491956.2462183"},{"key":"8_CR54","doi-asserted-by":"publisher","unstructured":"Souyris, J., Pavec, E.L., Himbert, G., Borios, G., J\u00e9gu, V., Heckmann, R.: Computing the worst case execution time of an avionics program by abstract interpretation. In: International Workshop on Worst-Case Execution Time Analysis, vol.\u00a01, pp. 21\u201324 (2007). https:\/\/doi.org\/10.4230\/OASIcs.WCET.2005.810","DOI":"10.4230\/OASIcs.WCET.2005.810"},{"key":"8_CR55","doi-asserted-by":"publisher","unstructured":"Stephens, N., et al.: Driller: augmenting fuzzing through selective symbolic execution. In: Network and Distributed System Security Symposium (2016). https:\/\/doi.org\/10.14722\/ndss.2016.23368","DOI":"10.14722\/ndss.2016.23368"},{"key":"8_CR56","doi-asserted-by":"publisher","unstructured":"Tristan, J.B., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. In: Symposium on Principles of Programming Languages, pp. 17\u201327 (2008). https:\/\/doi.org\/10.1145\/1328438.1328444","DOI":"10.1145\/1328438.1328444"},{"key":"8_CR57","unstructured":"Wang, T., Wei, T., Lin, Z., Zou, W.: Intscope: automatically detecting integer overflow vulnerability in X86 binary using symbolic execution. In: Network and Distributed System Security Symposium (2009)"},{"key":"8_CR58","doi-asserted-by":"publisher","unstructured":"Wartel, F., et al.: Measurement-based probabilistic timing analysis: lessons from an integrated-modular avionics case study. In: International Symposium on Industrial Embedded Systems, pp. 241\u2013248 (2013). https:\/\/doi.org\/10.1109\/SIES.2013.6601497","DOI":"10.1109\/SIES.2013.6601497"},{"key":"8_CR59","unstructured":"Waterman, A., Lee, Y., Patterson, D.A., Asanovi\u0107, K.: The RISC-V instruction set manual, volume I: User-level ISA, version 2.1. Technical Report. UCB\/EECS-2016-118, EECS Department, University of California, Berkeley (2016). https:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2016\/EECS-2016-118.pdf"},{"key":"8_CR60","doi-asserted-by":"publisher","unstructured":"Zhao, L., Li, G., De\u00a0Sutter, B., Regehr, J.: ARMor: fully verified software fault isolation. In: International Conference on Embedded Software, pp. 289\u2013298 (2011). https:\/\/doi.org\/10.1145\/2038642.2038687","DOI":"10.1145\/2038642.2038687"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T12:30:18Z","timestamp":1768307418000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_8","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":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}