×
Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen

Automating Event-B invariant proofs by rippling and proof patching. (English) Zbl 1425.68077

Formal Asp. Comput. 31, No. 1, 95-129 (2019).

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

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

Software:

Rodin; ProofPower; Z; IsaPlanner; IsaCoSy; Isabelle/HOL; Isabelle
Cite Review PDF
Full Text: DOI
OA License

References:

[1] Abrial, J.-R., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT12(6), 447-466 (2010) · doi:10.1007/s10009-010-0145-y
[2] Abrial, J.-R.: The B Book: assigning programs to meanings. Cambridge University Press, Cambridge (1996) · Zbl 0915.68015 · doi:10.1017/CBO9780511624162
[3] Abrial J-R (2007) A system development process with Event-B and the Rodin platform. In: ICFEM, pp 1-3
[4] Abrial, J.-R.: Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge (2010) · Zbl 1213.68214 · doi:10.1017/CBO9781139195881
[5] Arthan R, Jones RB. Z in HOL in ProofPower. BCS FACS FACTS, 2005-1
[6] Armando, A., Smaill, A., Green, I.: Automatic synthesis of recursive programs: the proof-planning paradigm. Autom Softw Eng6, 329-356 (1999) · doi:10.1023/A:1008763422061
[7] Bundy A, Basin D, Hutter D, Ireland A (2005) Rippling: meta-level guidance for mathematical reasoning, volume 56 of Cambridge tracts in theoretical computer science. Cambridge University Press · Zbl 1095.68108
[8] Bryans JW, Fitzgerald JS, McCutcheon T (2011) Refinement-based techniques in the analysis of information flow policies for dynamic virtual organisations. In: Camarinha-Matos LM, Pereira-Klen A, Afsarmanesh H (eds) Adaptation and value creating collaborative networks. Springer, pp 314-321
[9] Butler M, Hallerstede S (2007) The Rodin formal modelling tool. In:BCS-FACS
[10] Blanchette JC, Paulson LC (2018) Hammering Away. A User’s Guide to Sledgehammer for Isabelle/HOL. http://isabelle.in.tum.de/dist/doc/sledgehammer.pdf
[11] Bundy A (1998) A science of reasoning. In: International conference on automated reasoning with analytic tableaux and related methods · Zbl 0913.03022
[12] The Deploy project.http://www.deploy-project.eu/index.html. Accessed 2 Feb 2018
[13] Dixon L, Fleuriot JD (2003) IsaPlanner: a prototype proof planner in Isabelle. In: CADE
[14] Déharbe D, Fontaine P, Guyot Y, Voisin L (2012) SMT solvers for rodin. In: ABZ, pp 194-207
[15] Dixon L (2005) A proof planning framework for Isabelle. Ph.D. thesis, School of Informatics, University of Edinburgh
[16] Event-B and Rodin Documentation Wiki. Provers for Rodin.http://handbook.event-b.org/current/html/atelier_b_provers. Accessed 28 Feb 2015
[17] Grov G, Kissinger A, Lin Y (2013) A graphical language for proof strategies. In:LPAR, pp 324-339. Springer · Zbl 1406.68107
[18] Grov G, Lin Y (2017) The Tinker tool for graphical tactic development. Int J Softw Tools Technol Transf 1-17
[19] Hetzl S (2016) Why does induction require cut? Accessed 13 Aug 2016
[20] Heras J, Komendantskaya E, Johansson M, Maclean E (2013) Proof-pattern recognition and lemma discovery in ACL2. In: Logic for programming, artificial intelligence, and reasoning. Springer, pp 389-406 · Zbl 1407.68436
[21] Ireland, A., Bundy, A.: Productive use of failure in inductive proof. J Autom Reason16(1-2), 79-111 (1996) · Zbl 0847.68103 · doi:10.1007/BF00244460
[22] Ireland A, Grov G, Butler M (2010) Reasoned modelling critics: turning failed proofs into modelling guidance. In: ABZ, pp 189-202. Springer · Zbl 1264.68058
[23] Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J Autom Reason47(3), 251-289 (2011) · Zbl 1243.68268 · doi:10.1007/s10817-010-9193-y
[24] Jones, C.B.: Systematic software development using VDM, 2nd edn. Prentice Hall, Upper Saddle River (1990) · Zbl 0743.68048
[25] Johansson M, Rosén D, Smallbone N, Claessen K (2014) Hipster: integrating theory exploration in a proof assistant.In: CoRR, arXiv:1405.3426 · Zbl 1304.68157
[26] Lamport, L.: Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc, Boston (2002)
[27] Lin Y, Bundy A, Grov G (2012) The use of rippling to automate Event-B invariant preservation proofs. In: NASA formal methods, pp 231-236
[28] Lin Y (2015) The use of rippling to automate Event-B invariant preservation proofs. Ph.D. thesis
[29] Liang Y, Lin Y, Grov G (2016) “the Tinker” for Rodin. In: ABZ. Springer, pp 262-268
[30] Loomes M, Woodcock JCP (1988) Software engineering mathematics: formal methods demystified · Zbl 0825.68032
[31] Montano-RivasO, McCasland RL, Dixon L, Bundy A (2010) Scheme-based synthesis of inductive theories. In: MICAI, pp 348-361
[32] Paper source webpage for POPPA.http://www.sites.google.com/site/evalpoppa/. Accessed 4 Feb 2018
[33] Paulson LC (1994) Isabelle: a generic theorem prover, volume 828 ofLNCS. Springer · Zbl 0825.68059
[34] Rodin Proof Tactics. Functional overriding in goal.http://wiki.event-b.org/index.php/Rodin_Proof_Tactics. Accessed 2 Feb 2018
[35] Schmalz M (2012) Formalizing the logic of Event-B. Partial functions, definitional extensions, and automated theorem proving. Ph.D. thesis, ETH Zurich
[36] Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice Hall, London (1996) · Zbl 0855.68060
[37] Wright S (2009) Formal construction of instruction set architectures. Ph.D. thesis, University of Bristol, UK
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.