We report on a machine supported method for verifying safety properties of dynamic systems based on the first-order description of underlying state transition systems. By capturing a set of states by a state predicate, we can verify safety properties of infinite-state systems using predicate calculus in the set-theoretic iterative calculation of least fixpoints. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Mori, A., & Futatsugi, K. (2003). CafeOBJ as a tool for behavioral system verification. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2609, 461–470. https://doi.org/10.1007/3-540-36532-x_26
Mendeley helps you to discover research relevant for your work.