Formal verification and accelerated inference

Abstract

This paper proposes a method to transform of algorithm model presented in form of Kripke structure, as well as LTL-specification reflecting the algorithm requirements, into the knowledge base in language of first order predicate logic. This transformation makes it possible to use the studied algorithm of accelerated logical deduction inference methods in process of formal verification. Heuristic structure of such methods allows looking forward to the significant reduction of the overall time of verification with proper selection of the inference method and optimization of the formula specification syntactic tree. In addition, we propose a software system structure for verification of parallel algorithms based on technique ofmodel checking and described methods. The system has amodular architecture that allows for flexible change of the inference method, depending on specificity of analyzed algorithm.