CafeOBJ

swMATH6232MaRDI QIDQ18366FDOQ18366

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• A hidden Herbrand theorem: Combining the object and logic paradigms
• Transformation techniques for context-sensitive rewrite systems
• A Modular Equational Generalization Algorithm
• Stability of termination and sufficient-completeness under pushouts via amalgamation
• Equational formulas and pattern operations in initial order-sorted algebras
• Dynamic connectors for concurrency
• Title not available (Why is that?)
• Ground confluence of order-sorted conditional specifications modulo axioms
• Recent Trends in Algebraic Development Techniques
• Maude's module algebra
• Title not available (Why is that?)
• Foundations of Software Science and Computation Structures
• Relaxed models for rewriting logic
• Structured theories and institutions
• Term Rewriting and Applications
• Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
• Towards Formal Fault Tree Analysis Using Theorem Proving
• The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
• Non-intrusive Formal Methods and Strategic Rewriting for a Chemical Application
• Combining higher-order and first-order computation using \(\rho\)-calculus: Towards a semantics of ELAN
• Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
• Inductive behavioral proofs by unhiding
• Term Rewriting and Applications
• Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras
• Complete Categorical Deduction for Satisfaction as Injectivity
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Title not available (Why is that?)
• Initial semantics in logics with constructors
• Order-Sorted Parameterization and Induction
• Introducing \(H\), an institution-based formal specification and verification language
• Title not available (Why is that?)
• On combining algebraic specifications with first-order logic via Athena
• Matching Logic
• Birkhoff completeness for hybrid-dynamic first-order logic
• Ultraproducts and possible worlds semantics in institutions
• A modular order-sorted equational generalization algorithm
• Natural Rewriting for General Term Rewriting Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Order-Sorted Rewriting and Congruence Closure
• Foundations of logic programming in hybrid logics with user-defined sharing
• Title not available (Why is that?)
• Parchments for CafeOBJ Logics
• Two Algebraic Byways from Differential Equations: Gröbner Bases and Quivers
• A short overview of Hidden Logic
• Title not available (Why is that?)
• Formalizing provable anonymity in Isabelle/HOL
• Observational interpretations of hybrid dynamic logic with binders and silent transitions
• Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally
• Title not available (Why is that?)
• Borrowing interpolation
• Behavioural specification for hierarchical object composition
• FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY
• Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications
• An Institution for Imperative RSL Specifications
• Behavioral Rewrite Systems and Behavioral Productivity
• Title not available (Why is that?)
• Title not available (Why is that?)
• CafeOBJ Traces
• Towards a Combination of CafeOBJ and PAT
• Soundness in verification of algebraic specifications with OBJ
• Title not available (Why is that?)
• Web-based support for cooperative software engineering
• A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
• Addressed term rewriting systems: application to a typed object calculus
• From Domain to Requirements
• Verifying Security Protocols for Sensor Networks Using Algebraic Specification Techniques
• Title not available (Why is that?)
• Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method
• Towards behavioral Maude: behavioral membership equational logic
• Title not available (Why is that?)
• Rewriting-based verification of authentication protocols
• A rewriting logic approach to operational semantics (extended abstract)
• On Automation of OTS/CafeOBJ Method
• A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method
• Parameterized theories and views in full Maude 2. 0
• Theoretical Aspects of Computing – ICTAC 2005
• Twenty years of rewriting logic
• CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
• Strict coherence of conditional rewriting modulo axioms
• Title not available (Why is that?)
• Category-based constraint logic
• Proving Termination in the Context-Sensitive Dependency Pair Framework
• Title not available (Why is that?)
• Foundations for structuring behavioural specifications
• A Transformational Approach to Prove Outermost Termination Automatically
• Proving operational termination of membership equational programs
• Structural induction in institutions
• A rewriting logic approach to operational semantics
• An Institution-independent Generalization of Tarski's Elementary Chain Theorem
• Bisimulation and Hidden Algebra
• Semantic foundations for generalized rewrite theories
• Order-Sorted Generalization
• Automatic synthesis of logical models for order-sorted first-order theories
• Principles of proof scores in CafeOBJ
• Title not available (Why is that?)
• Foundations of algebraic specification and formal software development.
• Specification of real-time and hybrid systems in rewriting logic

This page was built for software: CafeOBJ