Thorough Checking Revisited

Recent years have seen a proliferation of 3-valued or capturing abstractions of systems, since these enable verifying both universal and existential properties. Reasoning about such systems is either inexpensive and imprecise (compositional checking), or expensive and precise (thorough checking). In this paper, we prove that thorough and compositional checks for temporal formulas in their disjunctive forms coincide, which leads to an effective procedure for thorough checking of a variety act models and the entire

• Type: Conference
• Year: 2006
• Where: FMCAD
• Authors: Shiva Nejati, Mihaela Gheorghiu, Marsha Chechik
• Keywords: Compositional Checking, FMCAD 2006, Formal Methods, Thorough Checking, Variety Act Models