Automating Event-B invariant proofs by rippling and proof patching

DOI10.1007/s00165-018-00476-7zbMath1425.68077WikidataQ113906136 ScholiaQ113906136MaRDI QIDQ667526

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

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

zbMATH Keywords

automated reasoning; formal verification; rippling; Event-B; lemma conjecturing

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

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