2 papers
cs.LO2026
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
Mathias Preiner, Aina Niemetz, Clark Barrett
Reasoning about array data structures is a key requirement for many applications in hardware and software verification, especially in combination with machine integers. The Satisfi…
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…