Decision Procedures for the Formal Analysis of Software