Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
From MaRDI portal
Publication:5738912
DOI10.1145/371282.371364zbMath1365.68317arXivcs/9910014OpenAlexW2118154221MaRDI QIDQ5738912
Miroslav N. Velev, Randal E. Bryant, Steven M. German
Publication date: 13 June 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/cs/9910014
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
NuMDG: a new tool for multiway decision graphs construction ⋮ Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Transforming equality logic to propositional logic ⋮ Producing and verifying extremely large propositional refutations ⋮ A Term Rewriting Technique for Decision Graphs ⋮ Building small equality graphs for deciding equality logic with uninterpreted functions ⋮ Zero, successor and equality in BDDs ⋮ Theory decision by decomposition ⋮ A New Approach for the Construction of Multiway Decision Graphs ⋮ The small model property: How small can it be? ⋮ Distributing the Workload in a Lazy Theorem-Prover
