Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
From MaRDI portal
Publication:5738912
DOI10.1145/371282.371364zbMath1365.68317arXivcs/9910014MaRDI 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
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs, Transforming equality logic to propositional logic, A Term Rewriting Technique for Decision Graphs, A New Approach for the Construction of Multiway Decision Graphs, Producing and verifying extremely large propositional refutations, Theory decision by decomposition, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Parallelizing SMT solving: lazy decomposition and conciliation, Zero, successor and equality in BDDs, The small model property: How small can it be?, NuMDG: a new tool for multiway decision graphs construction, Building small equality graphs for deciding equality logic with uninterpreted functions, Distributing the Workload in a Lazy Theorem-Prover
