AUTOMATED REASONING TECHNIQUES FOR SYSTEM CORRECTNESS VERIFICATION

The functionality and complexity of software and hardware systems are steadily growing. Consequently, the probability of delicate faults existence in these systems is also rising. Some of these faults may result in a destructive loss of money and time. However, one major goal of designing those systems is to construct improved and more reliable systems, regardless of the level of their complexity. Automated reasoning techniques and formal proving methods seems to be a promising approach to specify such systems and be automated to verify them. In this paper, we introduce and show how we can use some of those automated reasoning techniques and formal proving methods, using Propositional Logic (PL) and First Order Logic (FOL), in specifying and verifying the correctness of some properties related to such systems.