Formal Verification and Accelerated Inference

  • Dmitry Strabykin
  • Vasily Meltsov
  • Maria Dolzhenkova
  • Gennady Chistyakov
  • Alexey KuvaevEmail author
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 464)


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 of model checking and described methods. The system has a modular architecture that allows for flexible change of the inference method, depending on specificity of analyzed algorithm.


Formal verification Model checking Inference Disjunct dividing method 



The work was supported by the RFBR (project N 15-01-02818 a).


  1. 1.
    Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge, Mass. (2008)Google Scholar
  2. 2.
    Karpov, Y.: Model checking: Verifikatsiya parallel’nykh i raspredelennykh programmnykh sistem (Model checking. Verication of parallel and distributed software systems). BHV Petersburg, Saint Petersburg (2010)Google Scholar
  3. 3.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. Verication with Model Checking and Inference. MIT Press, Cambridge, Mass. (1999)Google Scholar
  4. 4.
    Fujita, M., Ghosh, I., Prasad, M.: Verification Techniques for System Level Design. Morgan Kaufmann Publishers, Amsterdam (2008)Google Scholar
  5. 5.
    Drechsler, R.: Advanced Formal Verification. Kluwer Academic Publishers, Boston (2004)CrossRefzbMATHGoogle Scholar
  6. 6.
    Zhang, Z., Li, Z., Chen, Y., Liu, G.: An automatic program verifier for PointerC: design and implementation. J. Comput. Res. Dev. 50(5), 1044–1054 (2013)MathSciNetGoogle Scholar
  7. 7.
    Dolzhenkova, M.L., Strabykin, D.A.: Deductive logical inference of the conclusions with creation of the scheme of a logical inference. J. Sci. Tech. Gazette Volga 4, 143–150 (2013)Google Scholar
  8. 8.
    Polikarpova, N., Shalyto, A.: Avtomatnoye programmirovaniye (Machine Programming). Piter, Saint Petersburg (2011)Google Scholar
  9. 9.
    Meltsov, V., Chistyakov, G.: Formalnaya verificatsia algoritmov s pomochyu technici proverki modeley i metodov logicheskogo vyvoda (Formal algorithm verification using model checking technique and inference methods). VINITI RAN, 358-B2013. Moscow (2013)Google Scholar
  10. 10.
    Huth, M., Ryan, M.: Logic in Computer Science, 2nd edn. Cambridge University Press, Cambridge [England] (2004)Google Scholar
  11. 11.
    Mateescu, R., Monteiro, P., Dumas, E., De Jong, H.: CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. Theoret. Comput. Sci. 412, 2854–2883 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Strabykin, D.: Logical method for predicting situation development based on abductive inference. J. Comput. Syst. Sci. Int. 52(5), 759–763 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Caferra, R.: Logic for Computer Science and Artificial Intelligence. ISTE, London (2011)CrossRefzbMATHGoogle Scholar
  14. 14.
    Vagin, D.: Dostovernyy i pravdopodobnyy vyvod v intellektualnykh sistemakh (Reliable and Plausible Conclusion in Intelligent Systems). FizMatLit, Moscow (2008)Google Scholar
  15. 15.
    Meltsov, V.Yu.: High Performance Systems of Deductive Inference: Monograph, 216 pp. Science Book Publishing House, Yelm, WA, USA (2014)Google Scholar
  16. 16.
    Meltsov, V., Chistyakov, G.: Effective method for constructing optimized parse tree of temporal logic formulas of linear time. Trans. TSTU 18(4), 813–820 (2012)Google Scholar
  17. 17.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2004)Google Scholar
  18. 18.
    Shipitsyna, A.A., Meltsov, V.Yu.: An approach to designing intelligent test systems. In: European Conference on Innovations in Technical and Natural Sciences 2nd International Scientific Conference, pp. 28–33 (2014)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Dmitry Strabykin
    • 1
  • Vasily Meltsov
    • 1
  • Maria Dolzhenkova
    • 1
  • Gennady Chistyakov
    • 1
  • Alexey Kuvaev
    • 1
    Email author
  1. 1.Department of the Electronic Computing MachinesVyatka State UniversityKirovRussian Federation

Personalised recommendations