{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T10:23:00Z","timestamp":1779099780944,"version":"3.51.4"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319708478","type":"print"},{"value":"9783319708485","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_6","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T10:43:26Z","timestamp":1510310606000},"page":"70-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["Applying a Formal Method in Industry: A 25-Year Trajectory"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Lecomte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Deharbe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Etienne","family":"Prun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erwan","family":"Mottin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,11]]},"reference":[{"key":"6_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). www.SMT-LIB.org"},{"key":"6_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2011.11.014","volume":"280","author":"MV Benveniste","year":"2011","unstructured":"Benveniste, M.V.: On using B in the design of secure micro-controllers: an experience report. Electr. Notes Theor. Comput. Sci. 280, 3\u201322 (2011)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"6_CR3","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: 1st International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroc\u0142aw, Poland, August 2011"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: Verit: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Burdy, L., D\u00e9harbe, D., Prun, \u00c9.: Interfacing automatic proof agents in atelier B: introducing \u201ciapa\u201d. In: Dubois, C., Masci, P., M\u00e9ry, D. (eds.) Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016. EPTCS, vol. 240, pp. 82\u201390. Limassol, Cyprus, 8 November 2016","DOI":"10.4204\/EPTCS.240.6"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Conchon, S., Iguernelala, M.: Tuning the Alt-Ergo SMT Solver for B Proof Obli-gations, pp. 294\u2013297. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_27","DOI":"10.1007\/978-3-662-43652-3_27"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Falampin, J., Le-Dang, H., Leuschel, M., Mokrani, M., Plagge, D.: Improving railway data validation with prob. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 27\u201343. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-33170-1_4","DOI":"10.1007\/978-3-642-33170-1_4"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-33600-8_10","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2016","unstructured":"Hansen, D., Schneider, D., Leuschel, M.: Using B and prob for data validation projects. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 167\u2013182. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_10"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-540-68237-0_32","volume-title":"FM 2008: Formal Methods","author":"T Lecomte","year":"2008","unstructured":"Lecomte, T.: Safe and reliable metro platform screen doors control\/command systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 430\u2013434. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_32"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-04570-7_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"T Lecomte","year":"2009","unstructured":"Lecomte, T.: Applying a formal method in industry: a 15-year trajectory. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 26\u201334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04570-7_3"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Lecomte, T.: Double c\u0153ur et preuve formelle pour automatismes sil4. 8E-Mod\u00e8les formels\/preuves formelles-s\u00fbret\u00e9 du logiciel (2016)","DOI":"10.4267\/2042\/61819"},{"key":"6_CR13","unstructured":"Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR abs\/1210.6815 (2012)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-30885-7_17","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D Mentr\u00e9","year":"2012","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.-C., Asuka, M.: Discharging proof obligations from atelier B using multiple automated provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 238\u2013251. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_17"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-33951-1_2","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"D Sabatier","year":"2016","unstructured":"Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 20\u201331. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_2"},{"issue":"4","key":"6_CR16","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The tptp problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337 (2009)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:36:50Z","timestamp":1570307810000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}