From the 1 of 6 linked papers with an AI index.
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
Romy Peled, Daniel Kroening, Michael Tautschnig +1
Large Language Models (LLMs) have shown potential for solving mathematical tasks. We show that LLMs can be utilized to generate proofs by induction for hardware verification and th…
cs.LO2026
Verifying the Rust Standard Library
Byron Cook, Remi Delmas, Zyad Hassan +9
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic…
cs.LO2024
Neural Model Checking
Mirco Giacobbe, Daniel Kroening, Abhinandan Pal +1
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every ex…