{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:53:23Z","timestamp":1725857603564},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319339504"},{"type":"electronic","value":"9783319339511"}],"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-33951-1_18","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T09:21:26Z","timestamp":1465896086000},"page":"243-253","source":"Crossref","is-referenced-by-count":3,"title":["Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Conchon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Iguernlala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"18_CR1","volume-title":"The B-book - Assigning Programs to Meanings","author":"J-R Abrial","year":"2005","unstructured":"Abrial, J.-R.: The B-book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Adjepon-Yamoah, D., Romanovsky, A., Iliasov, A.: A reactive architecture for cloud-based system engineering. In: Proceedings of the 2015 International Conference on Software and System Process, ICSSP 2015, pp. 77\u201381. ACM, New York, NY, USA (2015)","DOI":"10.1145\/2785592.2785611"},{"key":"18_CR3","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernlala, M., Lescuyer, S., Mebsout, A.: Alt-Ergo version\u00a00.99.1. CNRS, Inria, Universit\u00e9 Paris-Sud\u00a011, and OCamlPro, Dec 2014. http:\/\/alt-ergo.lri.fr\/ , http:\/\/alt-ergo.ocamlpro.com\/"},{"key":"18_CR4","unstructured":"ClearSy System Engineering. Atelier B User Manual, version\u00a04.0. http:\/\/tools.clearsy.com\/wp-content\/uploads\/sites\/8\/resources\/User_uk.pdf"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and groundAC completion modulo Shostak theories: design and implementation. Logical Methods Comput. Sci. 8(3), 653\u2013683 (2012)","DOI":"10.2168\/LMCS-8(3:16)2012"},{"issue":"2","key":"18_CR6","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/j.entcs.2008.04.080","volume":"198","author":"S Conchon","year":"2008","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): semantic combination of congruence closure with solvable theories. Electron. Notes Theor. Comput. Sci. 198(2), 51\u201369 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"18_CR7","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1016\/j.scico.2014.04.012","volume":"94","author":"D D\u00e9harbe","year":"2014","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in rodin. Sci. Comput. Program. 94, 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"18_CR10","unstructured":"The $$\\sf BWare$$ BWare Project (2012). http:\/\/bware.lri.fr\/"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-662-43652-3_1","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"L Voisin","year":"2014","unstructured":"Voisin, L., Abrial, J.-R.: The Rodin platform has turned ten. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 1\u20138. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:20:15Z","timestamp":1498321215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}