CIRC: A Behavioral Verification Tool Based on Circular Coinduction

DOI10.1007/978-3-642-03741-2_30MaRDI QIDQ2888503zbMATH OpenOpenAlexFDO

Authors Dorel Lucanu, Eugen-Ioan Goriac, Georgiana Caltais, Grigore Roşu

Publication date 1 June 2012

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-642-03741-2_30

Mathematics Subject Classification ID

Recommendations

• CIRC: A Circular Coinductive Prover
• scientific article; zbMATH DE number 1231661
• Computer Aided Verification
• Hidden coinduction: behavioural correctness proofs for objects
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 139813

Cites work

• A relative of the Thue-Morse sequence
• CIRC: A Circular Coinductive Prover
• Circular coinduction: a proof theoretical foundation
• Conditional circular coinductive rewriting with case analysis.
• scientific article; zbMATH DE number 1740032 (Why is no real title available?)
• Well-Definedness of Streams by Termination

Cited in

(22)

• CIRC
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Regular strategies as proof tactics for \textsf{CIRC}
• Circular coinduction: a proof theoretical foundation
• Stream differential equations: specification formats and solution methods
• Friends with benefits. Implementing corecursion in foundational proof assistants
• A Decision Procedure for Bisimilarity of Generalized Regular Expressions
• CIRC: A Circular Coinductive Prover
• A coalgebraic perspective on logical interpretations
• scientific article; zbMATH DE number 1231661 (Why is no real title available?)
• A Maude environment for CafeOBJ
• Fundamental Approaches to Software Engineering
• Quantitative Kleene coalgebras
• Circular coinduction in Coq using bisimulation-up-to techniques
• Behavioral rewrite systems and behavioral productivity
• On Automation of OTS/CafeOBJ Method
• Conditional circular coinductive rewriting with case analysis.
• Sound and complete equational reasoning over comodels
• Into the Infinite - Theory Exploration for Coinduction
• Proving behavioural apartness
• ``Backward coinduction, Nash equilibrium and the rationality of escalation
• Proving language inclusion and equivalence by coinduction

This page was built for publication: CIRC: A Behavioral Verification Tool Based on Circular Coinduction

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