Optimizing Bounded Model Checking for Linear Hybrid Systems

Bounded model checking (BMC) is an automatic verification method that is based on a finite unfolding of the system’s transition relation. BMC has been successfully applied, in particular, for discovering bugs in digital system design. Its success is based on the effectiveness of state-of-the-art satisfiability solvers that are used to check for a finite unfolding whether a violating state is reachable. In this paper we improve the BMC approach for linear hybrid systems based on lazy satisfiability solving. Our improvements follow two complementary directions. First, we optimize the formula representation of finite unfoldings of the transition relations of linear hybrid systems, and second, we accelerate the satisfiability checks by cumulating and generalizing data that is generated during earlier satisfiability checks. Experimental results show that the presented techniques accelerate the satisfiability checks significantly.

• Type: Conference
• Year: 2005
• Where: VMCAI
• Authors: Erika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen
• Keywords: Linear Hybrid Systems, Satisfiability Checks, Software Engineering, VMCAI 2005, finite Unfoldings