Automatic verification of sequential infinite-state processes

DOI10.1007/3-540-69678-4MaRDI QIDQ1377904zbMATH OpenFDO

Authors Olaf Burkart

Publication date 26 January 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-69678-4

zbMATH Keywords

equivalence checkingmodel checkingsequential processes

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Review text

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.

Recommendations

• Automated Technology for Verification and Analysis
• An automata-theoretic approach to reasoning about infinite-state systems
• Taming the infinite: Verification of infinite-state reactive systems by finitary means
• The automata-theoretic approach to verification of reactive systems

Cited in

(3)

• Automated verification of state sequence invariants in general game playing
• Verifying of interface assertions for infinite state Mealy machines
• Taming the infinite: Verification of infinite-state reactive systems by finitary means

This page was built for publication: Automatic verification of sequential infinite-state processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1377904)