CafeOBJ as a tool for behavioral system verification. 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.

References in zbMATH (referenced in 146 articles , 1 standard article )

Showing results 1 to 20 of 146.
Sorted by year (citations)

1 2 3 ... 6 7 8 next

  1. Găină, Daniel; Futatsugi, Kokichi: Initial semantics in logics with constructors (2015)
  2. Klein, Dominik: Key-secrecy of PACE with OTS/CafeOBJ (2015)
  3. Lucas, Salvador: Completeness of context-sensitive rewriting (2015)
  4. Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José: A modular order-sorted equational generalization algorithm (2014)
  5. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014)
  6. Diaconescu, Răzvan; Ţuţu, Ionuţ: Foundations for structuring behavioural specifications (2014)
  7. Găină, Daniel: Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally (2014)
  8. Găină, Daniel; Lucanu, Dorel; Ogata, Kazuhiro; Futatsugi, Kokichi: On automation of OTS/CafeOBJ method (2014)
  9. Ksystra, Katerina; Stefaneas, Petros; Frangos, Panayiotis: An algebraic framework for modeling of reactive rule-based intelligent agents (2014)
  10. Martins, Manuel A.; Madeira, Alexandre; Barbosa, Luís S.: The role of logical interpretations in program development (2014)
  11. Nakajima, Shin: Everlasting challenges with the OBJ language family (2014)
  12. Rocha, Camilo; Meseguer, José: Mechanical analysis of reliable communication in the alternating bit protocol using the maude invariant analyzer tool (2014)
  13. Stefaneas, Petros; Ouranos, Iakovos; Triantafyllou, Nikolaos; Ksystra, Katerina: Some engineering applications of the OTS/CafeOBJ method (2014)
  14. Ţuţu, Ionuţ: Parameterisation for abstract structured specifications (2014)
  15. Zhang, Min; Ogata, Kazuhiro; Futatsugi, Kokichi: Verifying the design of dynamic software updating in the OTS/CafeOBJ method (2014)
  16. Zhao, Yongxin; Dong, Jinsong; Liu, Yang; Sun, Jun: Towards a combination of CafeOBJ and PAT (2014)
  17. Ţuţu, Ionuţ: Comorphisms of structured institutions (2013)
  18. Diaconescu, Răzvan: Borrowing interpolation (2012)
  19. Diaconescu, Răzvan: An axiomatic approach to structuring specifications (2012)
  20. Futatsugi, Kokichi; Găină, Daniel; Ogata, Kazuhiro: Principles of proof scores in CafeOBJ (2012)

1 2 3 ... 6 7 8 next