Model Classifications and Automated Verification

Due to the significant progress in automated verification, there are often several techniques for a particular verification problem. In many circumstances different techniques are complementary -- each technique works well for different type of input instances. Unfortunately, it is not clear how to choose an appropriate technique for a specific instance of a problem. In this work we argue that this problem, selection of a technique and tuning its parameter values, should be considered as a standalone problem (a verification meta-search). We propose several classifications of models of asynchronous system and discuss applications of these classifications in the context of explicit finite state model checking.

• Type: Conference
• Year: 2007
• Where: FMICS
• Authors: Radek Pelánek
• Keywords: Explicit Finite State, FMICS 2007, Formal Methods, Particular Verification Problem, Significant Progress