1 citations · 1 across the 4 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Automating Bitvector and Finite Field Equivalence Proofs in Lean
Elizaveta Pertseva, Valentin Robert, Clark Barrett +1
Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and…
cs.LO2025
Integer Reasoning Modulo Different Constants in SMT
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor +4
This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving…