Publication:4818813
From MaRDI portal
zbMath1046.68605MaRDI QIDQ4818813
O. Shtrichman, Michael Siegel, Yoav Rodeh, Amir Pnueli
Publication date: 24 September 2004
equality logic; translation validation; uninterpreted functions; compiler verification; finite instantiation; range allocation
68Q60: Specification and verification (program logics, model checking, etc.)
03B25: Decidability of theories and sets of sentences
Related Items
Transforming equality logic to propositional logic, EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas, A Term Rewriting Technique for Decision Graphs, A New Approach for the Construction of Multiway Decision Graphs, Translation and run-time validation of loop transformations, Combining nonstably infinite theories, A framework for satisfiability modulo theories, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Zero, successor and equality in BDDs, NuMDG: a new tool for multiway decision graphs construction, Building small equality graphs for deciding equality logic with uninterpreted functions, Generalizing DPLL and satisfiability for equalities, Satisfiability Modulo Theories
Uses Software