Bang for the buck: Improvising and scheduling verification engines for effective resource utilization

In practice, verification engines have to solve many checkers in a very tight time budget, especially, when the system to be analyzed is large, with many coverage criteria. To cope with such a situation, we propose improved and light-weight verification techniques that are built over the state-of-the-art engines such as bounded model checking (BMC), induction, and guided-simulation (directed testing). Specifically, we propose using control state reachability (CSR) information—obtained from a given software system—to strengthen our induction-based proof engine. We also propose identifying and using lighthouses (or guide-posts)—intermediate control states—to simplify and reduce BMC instances, and to guide a simulation engine. We schedule these engines suitably to maximize the resource utilization. We implemented our techniques in a tool ACE, and integrated it in an industry strength software verification platform F-Soft to provide a robust and precise analysis framework. We show effectiveness of ACE on several industry and public benchmarks in a comparative study.