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 152 articles , 1 standard article )

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

1 2 3 ... 6 7 8 next

  1. Ferreirim, Isabel; Martins, Manuel A.: A short overview of hidden logic (2018)
  2. Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
  3. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
  4. Găină, Daniel: Foundations of logic programming in hybrid logics with user-defined sharing (2017)
  5. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  6. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
  7. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  8. Diaconescu, Răzvan: Functorial semantics of first-order views (2016)
  9. Lucas, Salvador; Meseguer, José: Normal forms and normal theories in conditional rewriting (2016)
  10. Meseguer, José: Order-sorted rewriting and congruence closure (2016)
  11. Ahmed, Waqar; Hasan, Osman: Towards formal fault tree analysis using theorem proving (2015)
  12. Găină, Daniel; Futatsugi, Kokichi: Initial semantics in logics with constructors (2015)
  13. Klein, Dominik: Key-secrecy of PACE with OTS/CafeOBJ (2015) ioport
  14. Lucas, Salvador: Completeness of context-sensitive rewriting (2015)
  15. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2015)
  16. Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José: A modular order-sorted equational generalization algorithm (2014)
  17. Belzner, Lenz; De Nicola, Rocco; Vandin, Andrea; Wirsing, Martin: Reasoning (on) service component ensembles in rewriting logic (2014) ioport
  18. Diaconescu, Răzvan: CafeOBJ traces (2014)
  19. Diaconescu, Răzvan; Ţuţu, Ionuţ: Foundations for structuring behavioural specifications (2014)
  20. Durán, Francisco; Roldán, Manuel; Moreno, Antonio; Álvarez, José María: Dynamic validation of maude prototypes of UML models (2014) ioport

1 2 3 ... 6 7 8 next