Reduced functional consistency of uninterpreted functions

MaRDI QIDQ2848689zbMATH OpenFDO

Authors Amir Pnueli, Ofer Strichman

Publication date 26 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066106000077

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Building small equality graphs for deciding equality logic with uninterpreted functions
• Artificial Intelligence and Symbolic Computation
• scientific article; zbMATH DE number 1796130
• To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$

Cited in

(5)

• Incremental bounded model checking for embedded software
• EUFORIA: complete software model checking with uninterpreted functions
• scientific article; zbMATH DE number 1870123 (Why is no real title available?)
• What's decidable about program verification modulo axioms?
• To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$

This page was built for publication: Reduced functional consistency of uninterpreted functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848689)