Quantification of Formal Properties for Productive Automotive Microcontroller Verification