On Automation of OTS/CafeOBJ Method

DOI10.1007/978-3-642-54624-2_29zbMath1407.68308OpenAlexW29114720MaRDI QIDQ5403084

Dorel Lucanu, Kokichi Futatsugi, Daniel Găină, Kazuhiro Ogata

Publication date: 25 March 2014

Published in: Specification, Algebra, and Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-54624-2_29

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items (1)

Generic Proof Scores for Generate & Check Method in CafeOBJ

Uses Software

• CIRC
• CafeOBJ
• Maude
• CITP

Cites Work

• Unnamed Item
• Unnamed Item
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Specifications in an arbitrary institution
• Logical foundations of CafeOBJ
• Logical systems for structured specifications.
• Observational logic, constructor-based logic, and their duality.
• Principles of proof scores in CafeOBJ
• Constructor-based observational logic
• Constructor-Based Inductive Theorem Prover
• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• Order-Sorted Parameterization and Induction
• Institutions: abstract model theory for specification and programming
• Initial semantics in logics with constructors

This page was built for publication: On Automation of OTS/CafeOBJ Method