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

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

1 2 3 ... 7 8 9 next

  1. Hennicker, Rolf; Knapp, Alexander; Madeira, Alexandre: Observational interpretations of hybrid dynamic logic with binders and silent transitions (2021)
  2. Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
  3. Durán, Francisco; Meseguer, José; Rocha, Camilo: Ground confluence of order-sorted conditional specifications modulo axioms (2020)
  4. Găină, Daniel; Nakamura, Masaki; Ogata, Kazuhiro; Futatsugi, Kokichi: Stability of termination and sufficient-completeness under pushouts via amalgamation (2020)
  5. 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)
  6. Riesco, Adrián; Ogata, Kazuhiro: CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications (2020)
  7. Găină, Daniel; Ţuţu, Ionuţ: Birkhoff completeness for hybrid-dynamic first-order logic (2019)
  8. Hamana, Makoto: How to prove decidability of equational theories with second-order computation analyser SOL (2019)
  9. Ferreirim, Isabel; Martins, Manuel A.: A short overview of hidden logic (2018)
  10. Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
  11. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
  12. Găină, Daniel: Foundations of logic programming in hybrid logics with user-defined sharing (2017)
  13. Ksystra, Katerina; Triantafyllou, Nikos; Stefaneas, Petros: On combining algebraic specifications with first-order logic via Athena (2017)
  14. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  15. Meseguer, José: Strict coherence of conditional rewriting modulo axioms (2017)
  16. Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
  17. Riesco, Adrián; Ogata, Kazuhiro: A formal proof generator from semi-formal proof documents (2017)
  18. Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
  19. Roşu, Grigore: Matching logic (2017)
  20. Diaconescu, Răzvan: Functorial semantics of first-order views (2016)

1 2 3 ... 7 8 9 next