Automatic generation of compact formal properties for effective error detection. - Michele Bertasi; Giuseppe Di Guglielmo; Graziano Pravadelli (CODES+ISSS, 2013)