{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:20:42Z","timestamp":1743027642058,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319478456"},{"type":"electronic","value":"9783319478463"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47846-3_14","type":"book-chapter","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T02:53:57Z","timestamp":1476413637000},"page":"210-225","source":"Crossref","is-referenced-by-count":1,"title":["Proving Event-B Models with Reusable Generic Lemmas"],"prefix":"10.1007","author":[{"given":"Alexei","family":"Iliasov","sequence":"first","affiliation":[]},{"given":"Paulius","family":"Stankaitis","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Romanovsky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,15]]},"reference":[{"key":"14_CR1","unstructured":"Event-B and the Rodin Platform. http:\/\/www.event-b.org\/"},{"key":"14_CR2","unstructured":"Furst, A.: Event-B model of the Order\/Supply Chain A2A Communication. http:\/\/deploy-eprints.ecs.soton.ac.uk\/129\/"},{"key":"14_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"14_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modelling in Event-B","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modelling in Event-B. Cambridge University Press, Cambridge (2010)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-642-39698-4_5","volume-title":"Theories of Programming and Formal Methods","author":"M Butler","year":"2013","unstructured":"Butler, M., Maamria, I.: Practical theory extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 67\u201381. Springer, Heidelberg (2013)"},{"key":"14_CR7","unstructured":"Clearsy. Atelier B.: User and Reference Manuals. http:\/\/www.atelierb.societe.com\/index_uk.html"},{"key":"14_CR8","unstructured":"March\u00e9, C., Paskevich, A., Bobot, F., Filli\u00e2tre, J.-C.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364, August 2011"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-540-87603-8_11","volume-title":"Abstract State Machines, B and Z","author":"S Hallerstede","year":"2008","unstructured":"Hallerstede, S.: On the purpose of Event-B proof obligations. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 125\u2013138. Springer, Heidelberg (2008)"},{"key":"14_CR10","unstructured":"Hoang, T.S.: Proof hints for Event-B (2012). CoRR, abs\/1211.1172"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-662-46823-4_14","volume-title":"Perspectives of Systems Informatics","author":"A Iliasov","year":"2015","unstructured":"Iliasov, A., Bryans, J.: A proof-based method for modelling timed systems. In: Voronkov, A., Virbitskaite, I. (eds.) PSI 2014. LNCS, vol. 8974, pp. 161\u2013176. Springer, Heidelberg (2015)"},{"key":"14_CR12","unstructured":"Industrial deployment of system engineering methods providing high dependability and productivity (DEPLOY), IST FP7 project. http:\/\/www.deploy-project.eu\/"},{"key":"14_CR13","unstructured":"Burdy, L.: Automatic refinement. In: Proceedings of BUGM at FM 1999 (1999)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Conchon, S., Contejean, \u00c9., Kanig, J., Lescuyer, S.: CC(X): semantical combination of congruence closure with solvable theories. In: Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), vol. 198, no. 2 of Electronic Notes in Computer Science, pp. 51\u201369. Elsevier Science Publishers (2008)","DOI":"10.1016\/j.entcs.2008.04.080"},{"key":"14_CR15","unstructured":"Rigorous Open Development Environment for Complex Systems (RODIN), IST FP6 STREP project. http:\/\/rodin.cs.ncl.ac.uk\/"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-33600-8_21","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Iliasov","year":"2016","unstructured":"Iliasov, A., Stankaitis, P., Adjepon-Yamoah, D., Romanovsky, A.: Rodin platform Why3 plug-in. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 275\u2013281. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-33600-8_21"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1007\/978-3-642-05089-3_37","volume-title":"FM 2009: Formal Methods","author":"MY Said","year":"2009","unstructured":"Said, M.Y., Butler, M., Snook, C.: Language and tool support for class and state machine refinement in UML-B. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 579\u2013595. Springer, Heidelberg (2009)"},{"key":"14_CR18","unstructured":"Hoang, T.S.: Event-B model of the Buyer\/Seller B2B Communication. http:\/\/deploy-eprints.ecs.soton.ac.uk\/128\/"},{"key":"14_CR19","unstructured":"The RODIN platform. http:\/\/rodin-b-sharp.sourceforge.net\/"},{"key":"14_CR20","unstructured":"TPTP: Thousands of Problems for Theorem Provers. www.tptp.org\/"},{"issue":"Part 2","key":"14_CR21","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D Deharbe","year":"2014","unstructured":"Deharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in Rodin. Sci. Comput. Program. 94(Part 2), 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Freitas, L., Whiteside, I.: Proof patterns for formal methods. In: Proceedings of FM 2014: Formal Methods - 19th International Symposium, Singapore, 12\u201316 May 2014, pp. 279\u2013295 (2014)","DOI":"10.1007\/978-3-319-06410-9_20"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47846-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T11:53:42Z","timestamp":1568462022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47846-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319478456","9783319478463"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47846-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}