Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study

Mikhail. A Lukin, Maxim Buzdalov, A. A. Shalyto

Research output: Chapter in Book/Report/Conference proceedingConference Proceeding (Non-Journal item)


Engineering of mission critical software requires a program to be verified that it satisfies a number of properties. This is often done using model checking. However, construction of a program model to be verified and analyzing counterexamples is not an easy task. This can be made easier with the automata-based programming paradigm.

There exist some cases when there are many programs to verify and it is impossible to construct a precise enough finite-state model of the environment. We present an approach for automata program verification under such conditions. Our case study is based on 800 automata programs which solve a simple path-planning problem. As a result, we verified that at least 231 of them are provably correct.
Original languageEnglish
Title of host publicationHardware and Software
Subtitle of host publicationVerification and Testing 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings
PublisherSpringer Nature
Number of pages6
ISBN (Electronic)978-3-319-13338-6
ISBN (Print)978-3-319-13337-9
Publication statusPublished - 06 Nov 2014
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Nature
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • automata-based programming
  • formal verification
  • model checking


Dive into the research topics of 'Formal Verification of 800 Genetically Constructed Automata Programs: A Case Study'. Together they form a unique fingerprint.

Cite this