CafeOBJ

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

Showing results 1 to 20 of 169.
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. Găină, Daniel; Nakamura, Masaki; Ogata, Kazuhiro; Futatsugi, Kokichi: Stability of termination and sufficient-completeness under pushouts via amalgamation (2020)
  4. 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)
  5. Riesco, Adrián; Ogata, Kazuhiro: CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications (2020)
  6. Găină, Daniel; Ţuţu, Ionuţ: Birkhoff completeness for hybrid-dynamic first-order logic (2019)
  7. Hamana, Makoto: How to prove decidability of equational theories with second-order computation analyser SOL (2019)
  8. Ferreirim, Isabel; Martins, Manuel A.: A short overview of hidden logic (2018)
  9. Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
  10. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
  11. Găină, Daniel: Foundations of logic programming in hybrid logics with user-defined sharing (2017)
  12. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  13. Meseguer, José: Strict coherence of conditional rewriting modulo axioms (2017)
  14. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
  15. Riesco, Adrián; Ogata, Kazuhiro: A formal proof generator from semi-formal proof documents (2017)
  16. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  17. Roşu, Grigore: Matching logic (2017)
  18. Diaconescu, Răzvan: Functorial semantics of first-order views (2016)
  19. Lucas, Salvador; Meseguer, José: Normal forms and normal theories in conditional rewriting (2016)
  20. Meseguer, José: Order-sorted rewriting and congruence closure (2016)

1 2 3 ... 7 8 9 next