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

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

1 2 3 ... 7 8 9 next

  1. Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
  2. Durán, Francisco; Meseguer, José; Rocha, Camilo: Ground confluence of order-sorted conditional specifications modulo axioms (2020)
  3. Iohara, Kenji (ed.); Malbos, Philippe (ed.); Saito, Masa-Hiko (ed.); Takayama, Nobuki (ed.): Two algebraic byways from differential equations: Gröbner bases and quivers (2020)
  4. Găină, Daniel; Ţuţu, Ionuţ: Birkhoff completeness for hybrid-dynamic first-order logic (2019)
  5. Ferreirim, Isabel; Martins, Manuel A.: A short overview of hidden logic (2018)
  6. Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
  7. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
  8. Găină, Daniel: Foundations of logic programming in hybrid logics with user-defined sharing (2017)
  9. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  10. Meseguer, José: Strict coherence of conditional rewriting modulo axioms (2017)
  11. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
  12. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  13. Roşu, Grigore: Matching logic (2017)
  14. Diaconescu, Răzvan: Functorial semantics of first-order views (2016)
  15. Lucas, Salvador; Meseguer, José: Normal forms and normal theories in conditional rewriting (2016)
  16. Meseguer, José: Order-sorted rewriting and congruence closure (2016)
  17. Ahmed, Waqar; Hasan, Osman: Towards formal fault tree analysis using theorem proving (2015)
  18. Futatsugi, Kokichi: Generate & check method for verifying transition systems in CafeOBJ (2015)
  19. Găină, Daniel; Futatsugi, Kokichi: Initial semantics in logics with constructors (2015)
  20. Klein, Dominik: Key-secrecy of PACE with OTS/CafeOBJ (2015) ioport

1 2 3 ... 7 8 9 next