Automating Event-B invariant proofs by rippling and proof patching

DOI10.1007/S00165-018-00476-7MaRDI QIDQ667526zbMATH OpenOpenAlexWikidataFDO

Authors Alan Bundy, Gudmund Grov, Ewen Maclean, Yu-Hui Lin

Publication date 13 March 2019

Published in Formal Aspects of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s00165-018-00476-7

zbMATH Keywords

automated reasoningformal verificationEvent-Bripplinglemma conjecturing

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Empowering the Event-B method using external theories
• Artificial Intelligence and Symbolic Computation
• Patterns for refinement automation
• Proving Quicksort Correct in Event-B
• Experiments in program verification using Event-B

Cites work

• scientific article; zbMATH DE number 1189094 (Why is no real title available?)
• scientific article; zbMATH DE number 43208 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• A graphical language for proof strategies
• Conjecture synthesis for inductive theories
• Hipster: integrating theory exploration in a proof assistant
• Isabelle. A generic theorem prover
• Modeling in Event B. System and software engineering.
• Productive use of failure in inductive proof
• Proof-pattern recognition and lemma discovery in ACL2
• Reasoned modelling critics: turning failed proofs into modelling guidance
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• The B-Book

Describes a project that uses

Uses Software

• IsaCoSy
• Z
• Rodin
• ProofPower
• IsaPlanner
• Isabelle

This page was built for publication: Automating Event-B invariant proofs by rippling and proof patching

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