Automatic verification of sequential infinite-state processes
The short monograph -- based on the author's doctoral thesis -- discusses a theoretical framework for the verification of reactive, sequential infinite-state systems. These are typically nonterminating systems. The \textit{invariance} is key concept: it records what remains true throughout the execution of the program.
scientific article; zbMATH DE number 1110379