M. Burgin and A. Tandon (USA)
software verification, automaton, specification, heterogeneous algebra
Theoretical results in computer science show that there are no general methods of direct software verification. To overcome this restriction, researchers correspond to programs different kinds of abstract automata and use these automata for software verification. In this paper, an automata-algebraic approach to program specification, modeling, and verification is developed further. Algorithmic properties of automata-algebraic verification procedures are obtained to discern those problems that are solvable by these methods and those problems that are unsolvable. It is proved that for complete specifications algebraic correctness is a decidable property, while for specifications with equivalence relations this property is undecidable.
Important Links:
Go Back
