Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification

Paschal C. Amusuo, Owen Cochell, Taylor Le Lievre +3

Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded M…