Revisiting Literal Ordering in CAR-Based Model Checking

July. 2023 – Dec. 2024 Supervised by Ofer Strichman from Technion.

See: Paper, Paper(long)

We found that the performance of model checkers is sensitive to the assumption ordering.

We analyzed the reason theoretically, extended existing strategies and finally proposed new ones. The implementation of the new strategies could not only outperform other strategies, but also outperform other state-of-the-art bug-finding algorithms.