CafeOBJ

swMATH6232MaRDI QIDQ18366

No author found.

Related Items

FORMAL VALIDATION AND VERIFICATION OF ATOMIC RESOLUTION MICROSCOPE CONTROL AND TOPOGRAPHY ⋮ Bisimulation and Hidden Algebra ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler ⋮ Unnamed Item ⋮ Recent Trends in Algebraic Development Techniques ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A short overview of Hidden Logic ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Transformation techniques for context-sensitive rewrite systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Composing Hidden Information Modules over Inclusive Institutions ⋮ Automata, Languages and Programming ⋮ Theoretical Aspects of Computing – ICTAC 2005 ⋮ Term Rewriting and Applications ⋮ Term Rewriting and Applications ⋮ Unnamed Item ⋮ CafeOBJ Traces ⋮ Parchments for CafeOBJ Logics ⋮ Towards a Combination of CafeOBJ and PAT ⋮ Behavioral Rewrite Systems and Behavioral Productivity ⋮ An Institution for Imperative RSL Specifications ⋮ Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method ⋮ On Automation of OTS/CafeOBJ Method ⋮ Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ Unnamed Item ⋮ A Transformational Approach to Prove Outermost Termination Automatically ⋮ Two Algebraic Byways from Differential Equations: Gröbner Bases and Quivers ⋮ Unnamed Item ⋮ Initial semantics in logics with constructors ⋮ Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras ⋮ Operational Termination of Membership Equational Programs: the Order-Sorted Way ⋮ Behavioural reasoning for conditional equations ⋮ Proving Termination in the Context-Sensitive Dependency Pair Framework ⋮ A Dependency Pair Framework for A ∨ C-Termination ⋮ Proving Behavioral Refinements of COL-specifications ⋮ Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method ⋮ Complete Categorical Deduction for Satisfaction as Injectivity ⋮ Non-intrusive Formal Methods and Strategic Rewriting for a Chemical Application ⋮ Web-based support for cooperative software engineering ⋮ Natural Rewriting for General Term Rewriting Systems ⋮ Addressed term rewriting systems: application to a typed object calculus ⋮ Order-Sorted Generalization ⋮ Foundations of Software Science and Computation Structures ⋮ Automated Reasoning ⋮ Unnamed Item ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Category-based constraint logic ⋮ Matching Logic ⋮ Unnamed Item ⋮ Foundations of logic programming in hybrid logics with user-defined sharing ⋮ Rewriting logic: Roadmap and bibliography ⋮ Borrowing interpolation ⋮ Constructor-based observational logic ⋮ Structured theories and institutions ⋮ Interpolation in Grothendieck institutions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ Ultraproducts and possible worlds semantics in institutions ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Towards Formal Fault Tree Analysis Using Theorem Proving ⋮ Algebraic simulations ⋮ Quasi-Boolean encodings and conditionals in algebraic specification ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Order-Sorted Parameterization and Induction ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Functorial semantics of first-order views ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic ⋮ An Algebraic Framework for Modeling of Reactive Rule-Based Intelligent Agents ⋮ A formal proof generator from semi-formal proof documents ⋮ Maude's module algebra ⋮ Birkhoff completeness for hybrid-dynamic first-order logic ⋮ Foundations of algebraic specification and formal software development. ⋮ Parameterisation for abstract structured specifications ⋮ Principles of proof scores in CafeOBJ ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications ⋮ Twenty years of rewriting logic ⋮ Unnamed Item ⋮ Foundations for structuring behavioural specifications ⋮ From Domain to Requirements ⋮ Coinduction for preordered algebra ⋮ Unnamed Item ⋮ On combining algebraic specifications with first-order logic via Athena ⋮ An axiomatic approach to structuring specifications ⋮ Verifying Security Protocols for Sensor Networks Using Algebraic Specification Techniques ⋮ A modular order-sorted equational generalization algorithm ⋮ Computationally Equivalent Elimination of Conditions ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ Comorphisms of structured institutions ⋮ Domain science and engineering from computer science to the sciences of informatics. II: Science ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Domain science and engineering from computer science to the sciences of informatics. I: Engineering ⋮ Completeness of context-sensitive rewriting ⋮ Observational interpretations of hybrid dynamic logic with binders and silent transitions ⋮ Equational abstractions ⋮ Domain Engineering ⋮ Soundness in verification of algebraic specifications with OBJ ⋮ Institution-independent model theory ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ A Maude environment for CafeOBJ ⋮ Unnamed Item ⋮ Forcing, downward Löwenheim-Skolem and omitting types theorems, institutionally ⋮ Unnamed Item ⋮ Grothendieck institutions ⋮ Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications ⋮ Institution morphisms ⋮ On the algebra of structured specifications ⋮ Behavioral abstraction is hiding information ⋮ Unnamed Item ⋮ Proving operational termination of membership equational programs ⋮ Structural induction in institutions ⋮ Semantic foundations for generalized rewrite theories ⋮ An encoding of partial algebras as total algebras ⋮ Saturated models in institutions ⋮ All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. ⋮ Normal forms and normal theories in conditional rewriting ⋮ Integrating Maude into Hets ⋮ CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications ⋮ A Modular Equational Generalization Algorithm ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ A semantic approach to interpolation ⋮ HasCasl: integrated higher-order specification and program development ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ A rewriting logic approach to operational semantics ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Extra theory morphisms for institutions: Logical semantics for multi-paradigm languages ⋮ Swinging types=functions+relations+transition systems ⋮ A hidden agenda ⋮ Towards Behavioral Maude ⋮ Operational termination of conditional term rewriting systems ⋮ Vivid: a framework for heterogeneous problem solving ⋮ Behavioural specification for hierarchical object composition ⋮ An Institution-independent Generalization of Tarski's Elementary Chain Theorem ⋮ Relating CASL with other specification languages: the institution level. ⋮ Relaxed models for rewriting logic ⋮ A hidden Herbrand theorem: Combining the object and logic paradigms ⋮ The role of logical interpretations in program development ⋮ A Rewriting Logic Approach to Operational Semantics (Extended Abstract) ⋮ Dynamic connectors for concurrency ⋮ Maude: specification and programming in rewriting logic ⋮ Logical foundations of CafeOBJ ⋮ Comparing logics for rewriting: Rewriting logic, action calculi and tile logic ⋮ Specification of real-time and hybrid systems in rewriting logic ⋮ Formalizing provable anonymity in Isabelle/HOL

This page was built for software: CafeOBJ