Automatic Generation of Compact Formal Properties for Effective Error Detection