Automating Event-B invariant proofs by rippling and proof patching
From MaRDI portal
Publication:667526
DOI10.1007/s00165-018-00476-7zbMath1425.68077OpenAlexW2908173533WikidataQ113906136 ScholiaQ113906136MaRDI QIDQ667526
Ewen Maclean, Alan Bundy, Gudmund Grov, Yu-Hui Lin
Publication date: 13 March 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-018-00476-7
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Conjecture synthesis for inductive theories
- Isabelle. A generic theorem prover
- Productive use of failure in inductive proof
- Reasoned modelling critics: turning failed proofs into modelling guidance
- A Graphical Language for Proof Strategies
- Proof-Pattern Recognition and Lemma Discovery in ACL2
- The B-Book
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Hipster: Integrating Theory Exploration in a Proof Assistant
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Automating Event-B invariant proofs by rippling and proof patching