3 citations · 5 across the 3 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2022★ 3 cited
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2
Mertcan Temel
Automatic and efficient verification of multiplier designs, especially through a provably correct method, is a difficult problem. We show how to utilize a theorem prover, ACL2, to…
cs.LO2020★ 2 cited
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2
Mertcan Temel
RP-Rewriter (Retain-Property) is a verified clause processor that can use some of the existing ACL2 rewrite rules to prove conjectures through term rewriting. Optimized for conject…