Functional Reduction to Speed Up Bounded Model Checking

Changyuan Yu, Wenbin Che, Hongce Zhang

Bounded model checking (BMC) is a widely used technique for formal property verification (FPV), where the transition relation is repeatedly unrolled to increasing depths and encode…