[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 |