Abstract:

Satisfiability Modulo Theories (SMT)based bounded model checking (BMC) has been considered as an improved technique to SATbased bounded model checking in recent years. Bounded model checking has often been used to check existential properties, but rarely used to verify global properties, and one of the reasons is that this method is hard to encode the global properties as its’ restricted by the bound. Therefore, In order to verify the global properties, the encodings in traditional bounded model checking should be changed. Combining with SMT, some global properties can be verified in real time systems. Experiments demonstrate the method is more efficient than existing methods.

Key words: bounded model checking;SMT;global properties;real time systems;verification