Searching for i-Good Lemmas to Accelerate Safety Model Checking

Published in CAV 2023, 2023

A new insight for improving the performance of SAT-based model checking. The definition of i-Good lemmas is simple but general, that can be proved to be effective in all state-of-the art model checkers, like Nu-XMV, IC3/PDR and SimpleCAR.

Recommended citation: Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu. (2023). “Searching for i-Good Lemmas to Accelerate Safety Model Checking.” CAV 2023.

Recommended citation: Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu. (2023). "Searching for i-Good Lemmas to Accelerate Safety Model Checking." CAV 2023.