Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications

DOI10.1007/978-3-319-17822-6_11zbMath1457.68066OpenAlexW2212580796MaRDI QIDQ2949707

Kazuhiro Ogata, Kokichi Futatsugi, Norbert Preining

Publication date: 2 October 2015

Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-17822-6_11

zbMATH Keywords

verificationlivenessalgebraic specificationCafeOBJ

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications

Uses Software

• CafeOBJ

Cites Work

• Linear temporal logic with until and next, logical consecutions
• Principles of proof scores in CafeOBJ
• Twenty years of rewriting logic
• Specification, algebra, and software. Essays dedicated to Kokichi Futatsugi
• Infinite-State Model Checking of LTLR Formulas Using Narrowing
• Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Predicate Abstraction of Rewrite Theories
• Generate & Check Method for Verifying Transition Systems in CafeOBJ
• Mechanizing UNITY in Isabelle

This page was built for publication: Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications