VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH UNIMOD.VERIFIER TOOL

Vadim Gurov, Bulat Jaminov

2008 , VOLUME 08, NUMBER 8 ( April )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH UNIMOD.VERIFIER TOOL

V. Gurov, B. Jaminov

Read the full article

Abstract

This article describes the verifier of automata-based programs created with the tool to support automata-based programming UniMod. Verifier works by integrating tool UniMod and verifier Bogor. Using developed verifier there is no need to convert automata-based program to the input language of the verifier. Requirements for the program are written in the language of temporal logic LTL.

Keywords: program verification, model checking, automata-based programming

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License