{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:38Z","timestamp":1785202238005,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319229683","type":"print"},{"value":"9783319229690","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22969-0_15","type":"book-chapter","created":{"date-parts":[[2015,8,20]],"date-time":"2015-08-20T08:51:42Z","timestamp":1440060702000},"page":"199-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["From Failure to Proof: The ProB Disprover for B and Event-B"],"prefix":"10.1007","author":[{"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jens","family":"Bendisposto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,21]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","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, New York (1996)"},{"key":"15_CR2","doi-asserted-by":"publisher","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, New York (2010)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"15_CR4","unstructured":"Andr\u00e9, P., Attiogb\u00e9, C., Lanoix, A.: Modelling and analysing the landing gear system: a solution with Event-B\/Rodin. http:\/\/www.lina.sciences.univ-nantes.fr\/aelos\/softwares\/LGS-ABZ2014\/index.php. Solution to ABZ-2014, Accessed: 17 March 2014"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"15_CR6","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (2010)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"CW Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Bendisposto, J., Krings, S., Leuschel, M.: Who watches the watchers: Validating the prob validation tool. In: Proceedings of the 1st Workshop on Formal-IDE, EPTCS XYZ, 2014, Electronic Proceedings in Theoretical Computer Science (2014)","DOI":"10.4204\/EPTCS.149.3"},{"key":"15_CR9","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","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":"15_CR10","series-title":"Lecture Notes in Computer Science","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-22. LNCS, vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"M Carlsson","year":"1997","unstructured":"Carlsson, M., Ottosson, G.: An open-ended finite domain constraint solver. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292. Springer, Heidelberg (1997)"},{"key":"15_CR12","unstructured":"ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France (2009). http:\/\/www.atelierb.eu\/"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-662-43652-3_27","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"S Conchon","year":"2014","unstructured":"Conchon, S., Iguernelala, M.: Tuning the Alt-Ergo SMT solver for B proof obligations. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 294\u2013297. Springer, Heidelberg (2014)"},{"key":"15_CR14","first-page":"217","volume":"2010","author":"D D\u00e9harbe","year":"2010","unstructured":"D\u00e9harbe, D.: Automatic verification for a class of proof obligations with SMT-solvers. Proceedings ASM 2010, 217\u2013230 (2010)","journal-title":"Proceedings ASM"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-662-43652-3_26","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Delahaye","year":"2014","unstructured":"Delahaye, D., Dubois, C., March\u00e9, C., Mentr\u00e9, D.: The BWare project: building a proof platform for the automated verification of B proof obligations. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 290\u2013293. Springer, Heidelberg (2014)"},{"issue":"4\u20135","key":"15_CR17","first-page":"767","volume":"11","author":"S Hallerstede","year":"2011","unstructured":"Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4\u20135), 767\u2013782 (2011)","journal-title":"TPLP"},{"key":"15_CR18","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","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":"15_CR19","unstructured":"Konrad, M., Voisin, L.: Translation from set-theory to predicate calculus. Technical report, ETH Zurich (2011)"},{"key":"15_CR20","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1002\/9781119002727.ch14","volume-title":"Formal Methods Applied to ComplexSystems: Implementation of the B Method, Chap. 14","author":"M Leuschel","year":"2014","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the prob constraint solver 10. In: Boulanger, J.-L. (ed.) Formal Methods Applied to ComplexSystems: Implementation of the B Method, Chap. 14, pp. 427\u2013446. Wiley ISTE, Hoboken (2014)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45013-0","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. Springer, Heidelberg (2003)"},{"issue":"2","key":"15_CR22","doi-asserted-by":"publisher","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. Software Tools for Technology Transfer (STTT) 10(2), 185\u2013203 (2008)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"15_CR23","unstructured":"Ligot, O., Bendisposto, J., Leuschel, M.: Debugging Event-B Models using the ProB Disprover Plug-in. In: Proceedings AFADL 2007, June (2007)"},{"key":"15_CR24","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","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":"15_CR25","doi-asserted-by":"publisher","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":"15_CR26","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","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":"15_CR27","unstructured":"Weissenbacher, G., Kr\u00f6ning, D., R\u00fcmmer, P.: A proposal for a theory of finite sets, lists, and maps for the smt-lib standard. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT 2009 (2009)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22969-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T16:56:35Z","timestamp":1718038595000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22969-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319229683","9783319229690"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22969-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"21 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}