Combining Deduction and Model Checking Sample Clauses

Combining Deduction and Model Checking. The main advantage of theorem proving is its ability to reason about infinite state spaces and the main benefit of model checking is its ability to be implemented fully as an automatic tool. They can be composed to yield advanced techniques for verification such as abstraction and compositional reasoning. As a way to deal with the problem of state explosion, abstraction techniques have been proposed in order to integrate theorem proving and model checking [49, 104, 102]. The idea is to reduce the original system to a smaller model via interactive proof techniques. In a sec- ond step, the smaller system is analyzed using automatic model checking tools. Usually, the smaller system is obtained by partitioning the original state space via a structure-preserving function between the two state spaces called abstracting function. The theorem prover is em- ployed in order to guarantee the abstraction to be sound, that is if the abstract system satisfies a property, so does the original system [117]. Another way to overcome the state explosion problem is compositional reasoning tech- niques: decomposing the process of reasoning about the behavior of a composed system into partial reasonings about the behaviors of its constituents. For this purpose, the system and the desired property both are decomposed into components and local properties. The correctness of each local property of a component is verified by model checking, while showing that the correctness of local properties entails the correctness of the whole desired property is done by theorem proving [86, 123].