8 citations · 17 across the 3 of their papers we have counts for
3 papers
cs.LO2023★ 3 cited
Verus: Verifying Rust Programs using Linear Ghost Types (extended version)
Andrea Lattuada, Travis Hance, Chanhee Cho +6
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making R…
cs.PL2018★ 6 cited
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…
cs.PL2010★ 8 cited
Automated Verification of Practical Garbage Collectors
Chris Hawblitzel, Erez Petrank
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graph…