VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Abstract elided by the publisher.
Related papers
- Generically Automating Separation Logic by Functors, Homomorphisms, and Modules POPL 2025
- VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System PLDI 2026
- Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust CPP 2026
- The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems CAV 1997
- Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM TACAS 2025
- Verus: Verifying Rust Programs using Linear Ghost Types OOPSLA 2023
- Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant POPL 2015
- AutoVerus: Automated Proof Generation for Rust Code OOPSLA 2025