Michael Sammler

VIP: verifying real-world C idioms with integer-pointer casts

2022 · Proceedings of the ACM on Programming Languages

Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level ( e.g. , bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they …

DimSum: A Decentralized Approach to Multi-language Semantics and Verification

2023 · Proceedings of the ACM on Programming Languages

Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language …