2 papers
cs.PL2025
Automated Formal Verification of a Software Fault Isolation System
Matthew Sotoudeh, Zachary Yedidia
Software fault isolation (SFI) is a popular way to sandbox untrusted software. A key component of SFI is the verifier that checks the untrusted code is written in a subset of the m…
cs.PL2025
Automated Verification of Monotonic Data Structure Traversals in C
Matthew Sotoudeh
Bespoke data structure operations are common in real-world C code. We identify one common subclass, monotonic data structure traversals (MDSTs), that iterate monotonically through…