Title: THEOREM PROVING TECHNIQUES FOR FORMAL SYSTEM VERIFICATION

Year of Publication: Jun - 2012
Page Numbers: 19-27
Authors: Hasan Krad
Conference Name: The International Conference on Informatics and Applications (ICIA2012)
- Malaysia

Abstract:


The complexity and functionality of Hardware and Software systems are persistently growing. Therefore, the probability of subtle faults existence in these systems is also increasing. Some of these faults may result in a devastating loss in terms of money and time. However, one main goal of designing those systems is to construct better and more reliable systems, regardless of the level of their complexity. Formal 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 formal methods techniques, Propositional Logic (PL) and First Order Logic (FOL), in specifying and verifying the correctness of some properties related to such systems.