Software verification using hybrid explicit and symbolic model checking

摘要

A computer-implemented method for verifying a target system includes defining a specification including properties applicable to the target system. Execution sequences of the target system are identified. A set of the execution sequences is grouped into an equivalence class characterized by a common control flow. A symbolic representation of the equivalence class is evaluated so as to verify a compliance of the set of the execution sequences with one or more of the properties.