Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic

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

zbMATH Keywords

decision proceduresuninterpreted functionsprocessor verfication

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (13)

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

This page was built for publication: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic