{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:57:11Z","timestamp":1761929831068,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319336923"},{"type":"electronic","value":"9783319336930"}],"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-33693-0_23","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:35:47Z","timestamp":1464068147000},"page":"361-375","source":"Crossref","is-referenced-by-count":20,"title":["SMT Solvers for Validation of B and Event-B Models"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"23_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J-R Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An open extensible tool environment for Event-B. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588\u2013605. Springer, Heidelberg (2006)"},{"key":"23_CR4","unstructured":"Attiogb\u00e9, C., Lanoix, A.: Modelling and analysing the landing gear system: a solution with Event-B\/Rodin. Solution to ABZ 2014 case study (2014)"},{"key":"23_CR5","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":"23_CR6","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-07512-9_1","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"F Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1\u201318. Springer, Heidelberg (2014)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"issue":"1\u20132","key":"23_CR8","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1017\/S1471068411000482","volume":"12","author":"M Carlsson","year":"2012","unstructured":"Carlsson, M., Mildner, P.: Sicstus prolog \u2014 the first 25 years. Theor. Pract. Logic Program. 12(1\u20132), 35\u201366 (2012)","journal-title":"Theor. Pract. Logic Program."},{"key":"23_CR9","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":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012)"},{"issue":"Part 2","key":"23_CR11","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(Part 2), 130\u2013143 (2014)","journal-title":"Sci. Comput. Program."},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"issue":"4\u20135","key":"23_CR13","doi-asserted-by":"crossref","first-page":"767","DOI":"10.1017\/S1471068411000299","volume":"11","author":"S Hallerstede","year":"2011","unstructured":"Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. Theor. Pract. Logic Program. 11(4\u20135), 767\u2013782 (2011)","journal-title":"Theor. Pract. Logic Program."},{"key":"23_CR14","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/978-3-319-07512-9_5","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"D Hansen","year":"2014","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66\u201379. Springer, Heidelberg (2014)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-319-22969-0_15","volume-title":"Software Engineering and Formal Methods","author":"S Krings","year":"2015","unstructured":"Krings, S., Bendisposto, J., Leuschel, M.: From failure to proof: the ProB disprover for B and Event-B. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 199\u2013214. Springer, Heidelberg (2015)"},{"key":"23_CR16","unstructured":"Kr\u00f6ning, D., R\u00fcmmer, P., Weissenbacher, G.: A proposal for a theory of finite sets, lists, and maps for the SMT-LIB standard. In: Informal Proceedings SMT Workshop (2009)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Proceedings ACM SAC, pp. 615\u2013622 (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge D.: From animation to data validation: the prob constraint solver 10 years on. In: Boulanger, J.-L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, Chap. 14, pp. 427\u2013446. Wiley ISTE, Hoboken (2014)","DOI":"10.1002\/9781119002727.ch14"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"issue":"2","key":"23_CR20","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"23_CR21","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/978-3-319-07512-9_6","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"A Mammar","year":"2014","unstructured":"Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 80\u201394. Springer, Heidelberg (2014)"},{"issue":"1","key":"23_CR22","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/2406336.2406351","volume":"12","author":"D M\u00e9ry","year":"2013","unstructured":"M\u00e9ry, D., Singh, N.K.: Formal specification of medical systems by proof-based refinement. ACM Trans. Embed. Comput. Syst. 12(1), 15:1\u201315:25 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Moura, L.M.D., B\u00f8jrner. N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/978-3-642-32759-9_31","volume-title":"FM 2012: Formal Methods","author":"D Plagge","year":"2012","unstructured":"Plagge, D., Leuschel, M.: Validating B, Z and TLA+ using ProB and Kodkod. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372\u2013376. Springer, Heidelberg (2012)"},{"key":"23_CR25","volume-title":"The B-Method: An Introduction. Cornerstones of Computing","author":"S Schneider","year":"2001","unstructured":"Schneider, S.: The B-Method: An Introduction. Cornerstones of Computing. Palgrave, London (2001)"},{"key":"23_CR26","series-title":"Communications in Computer and Information Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-319-07512-9_2","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"W Su","year":"2014","unstructured":"Su, W., Abrial, J.-R.: Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 19\u201335. Springer, Heidelberg (2014)"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T19:06:09Z","timestamp":1748977569000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}