Specification, Algebra, and Software : essays dedicated to Kokichi Futatsugi

Domain Endurants: An Analysis and Description Process Model.- On Formal Definition and Analysis of Formal Verification Processes.- CafeOBJ Traces.- Parchments for CafeOBJ Logics.- Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications.- The Versatile Synchronous Observer.- Model Checking TLR* Guarantee Formulas on Infinite Systems.- Towards a Combination of CafeOBJ and PAT.-Negative Variables and the Essence of Object-Oriented Programming.- Reasoning (on) Service Component Ensembles in Rewriting Logic.- Dynamic Validation of Maude Prototypes of UML Models.- Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way).- The Semantics of Datalog for the Evidential Tool Bus (Extended Abstract).- Synthesis of Infinite-State Abstractions and Their Use for Software Validation.- Behavioral Rewrite Systems and Behavioral Productivity.- Functional Logic Programming in Maude.- Confluence: The Unifying, Expressive Power of Locality.- Foundations for Ensemble Modeling - The Helena Approach: Handling Massively Distributed Systems with ELaborate ENsemble Architectures.- Behaviour, Interaction and Dynamics.- Partially Ordered Knowledge Sharing and Fractionated Systems in the Context of other Models for Distributed Computing.- Extending Operation Semantics to Enhance the Applicability of Formal Refinement.- An Institution for Imperative RSL Specifications.- 8k-ary Grid Graph Models of Tabular Forms.- Everlasting Challenges with the OBJ Language Family.- Formal Modeling and Analysis of Google's Megastore in Real-Time Maude.- EHRA: Specification and Analysis of Energy-Harvesting Wireless Sensor Networks.- Some Engineering Applications of the OTS/CafeOBJ Method.- 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.