Regular Strategies as Proof Tactics for CIRC

DOI10.1016/j.entcs.2008.03.055zbMath1279.68056OpenAlexW1998735422MaRDI QIDQ2873678

Dorel Lucanu, Grigore Roşu, Gheorghe Grigoras

Publication date: 24 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.03.055

zbMATH Keywords

behavioral equivalencecircular coinductionproof tacticsregular strategies

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• CIRC
• Maude
• CoCasl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• Maude: specification and programming in rewriting logic
• Decidability of bisimulation equivalence for process generating context-free languages
• CIRC: A Circular Coinductive Prover
• Actions speak louder than words: proving bisimilarity for context-free processes
• Fundamental Approaches to Software Engineering
• Building program optimizers with rewriting strategies
• Recent Trends in Algebraic Development Techniques