27 citations · 33 across the 9 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
cs.PL2026
DueList: A Theory of Lists with Combinators for SMT Solvers
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
Formal verification tools commonly rely on SMT solvers to automatically reason about programs, leveraging a range of logical theories, e.g., linear integer arithmetic, arrays, or s…
cs.CR2026
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Son Ho, Cédric Fournet, Jonathan Protzenko +7
We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…