CIRC: A Circular Coinductive Prover

DOI10.1007/978-3-540-73859-6_25MaRDI QIDQ3612501zbMATH OpenOpenAlexFDO

Authors Dorel Lucanu, Grigore Roşu

Publication date 10 March 2009

Published in Algebra and Coalgebra in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73859-6_25

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• Regular strategies as proof tactics for \textsf{CIRC}
• Circular coinduction: a proof theoretical foundation
• Circular coinduction in Coq using bisimulation-up-to techniques
• Fundamental Approaches to Software Engineering

Cited in

(19)

• Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
• CIRC
• Non-well-founded deduction for induction and coinduction
• Integrating induction and coinduction via closure operators and proof cycles
• Behavioral and coinductive rewriting
• Regular strategies as proof tactics for \textsf{CIRC}
• Circular coinduction: a proof theoretical foundation
• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• A tool proving well-definedness of streams using termination tools
• Stream differential equations: specification formats and solution methods
• Well-Definedness of Streams by Termination
• Circuits as streams in Coq: verification of a sequential multiplier
• Patterns for Maude metalanguage applications
• A Maude environment for CafeOBJ
• Fundamental Approaches to Software Engineering
• Circular coinduction in Coq using bisimulation-up-to techniques
• Conditional circular coinductive rewriting with case analysis.
• Checking equivalence in a non-strict language
• Some techniques for reasoning automatically on co-inductive data structures

Describes a project that uses

Uses Software

• Maude

This page was built for publication: CIRC: A Circular Coinductive Prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612501)