Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
equality with uninterpreted functions and memories
scientific article; zbMATH DE number 2056553
scientific article