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.
Keywords for this software
References in zbMATH (referenced in 167 articles , 1 standard article )
Showing results 1 to 20 of 167.
Sorted by year (- Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
- Durán, Francisco; Meseguer, José; Rocha, Camilo: Ground confluence of order-sorted conditional specifications modulo axioms (2020)
- Găină, Daniel; Nakamura, Masaki; Ogata, Kazuhiro; Futatsugi, Kokichi: Stability of termination and sufficient-completeness under pushouts via amalgamation (2020)
- 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)
- Găină, Daniel; Ţuţu, Ionuţ: Birkhoff completeness for hybrid-dynamic first-order logic (2019)
- Hamana, Makoto: How to prove decidability of equational theories with second-order computation analyser SOL (2019)
- Ferreirim, Isabel; Martins, Manuel A.: A short overview of hidden logic (2018)
- Lucas, Salvador; Gutiérrez, Raúl: Automatic synthesis of logical models for order-sorted first-order theories (2018)
- Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors (2018)
- Găină, Daniel: Foundations of logic programming in hybrid logics with user-defined sharing (2017)
- Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
- Meseguer, José: Strict coherence of conditional rewriting modulo axioms (2017)
- Meseguer, José; Skeirik, Stephen: Equational formulas and pattern operations in initial order-sorted algebras (2017)
- Riesco, Adrián; Ogata, Kazuhiro: A formal proof generator from semi-formal proof documents (2017)
- Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
- Roşu, Grigore: Matching logic (2017)
- Diaconescu, Răzvan: Functorial semantics of first-order views (2016)
- Lucas, Salvador; Meseguer, José: Normal forms and normal theories in conditional rewriting (2016)
- Meseguer, José: Order-sorted rewriting and congruence closure (2016)
- Ahmed, Waqar; Hasan, Osman: Towards formal fault tree analysis using theorem proving (2015)