A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
scientific article; zbMATH DE number 5149171