"What is easy to unterstand is also easier to verify by machine" - SIC!2025
PISTIs-V
- J. Zhao, A. Legnani, T. T. Ung, H. Truong, T. W. Sau, M. Tanaka, J. A. Pohjola, T. Sewell, R. Sison, H. Syeda, M. Myreen, M. Norrish, and G. Heiser, Verifying device drivers with Pancake, arXiv preprint, Jan. 2025. doi: 10.48550/arXiv.2501.08249.
- L. Murphy, A. Rizaldi, L. Rossouw, C. George, J. Treloar, H. Pearce, M. Tanaka, and G. Heiser, High-fidelity specification of real-world devices, in PLOS '25: Proceedings of the 13th Workshop on Programming Languages and Operating Systems, Seoul, Republic of Korea, Oct. 2025, pp. 60-67. doi: 10.1145/3764860.3768335.
- R. Sison, Two interfaces for seL4 kernel verification: Time protection and the kernel–userland gap (extended abstract), in Isabelle Workshop, Jul. 2026. https://trustworthy.systems/publications/papers/Sison_26.pdf.
- J. Zhao, Mechanising local rely-guarantee reasoning over the seL4 trace monad, in Isabelle Workshop, Jul. 2026. https://trustworthy.systems/publications/papers/Zhao_26.pdf.
- S. Tyler, A. Legnani, J. Zhao, Z. Shen, R. Wu, M. Tanaka, and G. Heiser, SMT-based deductive verification of device drivers using the Pancake-to-Viper transpiler, in PLOS '26: Proceedings of the 14th Workshop on Programming Languages and Operating Systems, Sept. 2026, pp. 103-111. doi: 10.1145/3831586.3838153.
Formula-V
- F. Farka, C. Abate, S. Kan, and S. Ertel, "Debug, Execute, Verify! Development-Verification Co-Design Made Practical", in Proceedings of the 13th Workshop on Programming Languages and Operating Systems, Seoul/Republic of Korea: ACM, Oct. 2025, S. 51–59. doi: 10.1145/3764860.3768326.
- C. Abate, M. Elsheikh, K. Liotati, F. Farka and S. Ertel, "WP-Preserving Compilation -- Preserving Weakest Preconditions for End-to-End Verification", presented at 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026), Rennes/France, Jan. 2026. https://popl26.sigplan.org/details/prisc-2026-papers/4/WP-Preserving-Compilation-Preserving-Weakest-Preconditions-For-End-to-End-Verifica.
- S. Kan and S. Ertel, "Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification", arXiv:2605.04933v2, May 2026. doi: https://doi.org/10.48550/arXiv.2605.04933.
PROTECT
- A. VanHattum, D. Schwartz-Narbonne, N. Chong, and A. Sampson, „Verifying dynamic trait objects in rust“, in Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice, Pittsburgh Pennsylvania: ACM, Mai 2022, S. 321–330. doi: 10.1145/3510457.3513031.
- C. Ghinami, I.P. Tresolavy, L. Seibt, N. Bosbach, & R. Leupers, „Leveraging SystemC-TLM-based Virtual Prototypes for Embedded Software Fuzzing“, 2025, arXiv. doi: 10.48550/ARXIV.2509.01318.
- L. Deutschmann, A. Meza, D. Stoffel, W. Kunz, and R. K. Rptu, „FastPath: A Hybrid Approach for Efficient Hardware Security Verification“, in 2025 62nd ACM/IEEE Design Automation Conference (DAC), San Francisco, CA, USA: IEEE, Juni 2025, S. 1–7. doi: 10.1109/DAC63849.2025.11132905.
- P. Schmitz, T. Jauch, A. Wezel, M.R. Fadiheh, T. Tiemann, J. Heller, T. Eisenbarth, D. Stoffel, & W. Kunz, „Okapi: Efficiently Safeguarding Speculative Data Accesses in Sandboxed Environments“, in Proceedings of the 20th ACM Asia Conference on Computer and Communications Security, Hanoi Vietnam: ACM, Aug. 2025, S. 1203–1218. doi: 10.1145/3708821.3733869.
- C. Ghinami, I.P. Tresolavy, L. Seibt, N. Bosbach, & R. Leupers, "Stateful Embedded Fuzzing with Peripheral-Accurate SystemC Virtual Prototypes", 2026, arXiv. doi: 10.48550/arXiv.2604.19824.
- A. Wezel, J. Müller, L. Deutschmann, T. Jauch, P. Schmitz, A. L. Duque Antón, S. Czernitzki, M.R. Fadiheh, K. Devarajegowda, J. Bormann, D. Stoffel and W. Kunz, "DiamondBlade: Scalable Information Flow Tracking Based on Semantic Path Decomposition", 2026, IEEE International Test Conference (ITC), San Antonio, TX, USA.