3 papers
cs.PL2025
Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
Zachary Grannan, Aurea Bílá, Jonáš Fiala +4
Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability…
cs.PL2023
Resource Specifications for Resource-Manipulating Programs
Zachary Grannan, Alexander J. Summers
Specifications for modular program verifiers are expressed as constraints on program states (e.g. preconditions) and relations on program states (e.g. postconditions). For programs…
cs.PL2022
REST: Integrating Term Rewriting with Program Verification (Extended Version)
Zachary Grannan, Niki Vazou, Eva Darulova +1
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables fl…