{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T03:19:08Z","timestamp":1768965548266,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319989372","type":"print"},{"value":"9783319989389","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-98938-9_20","type":"book-chapter","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T11:08:34Z","timestamp":1533726514000},"page":"346-366","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Repair and Generation of Formal Models Using Synthesis"],"prefix":"10.1007","author":[{"given":"Joshua","family":"Schmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Krings","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York, NY, USA (1996)"},{"key":"20_CR2","unstructured":"Balog, M., Gaunt, A.L., Brockschmidt, M., Nowozin, S., Tarlow, D.: DeepCoder: learning to write programs. In: 5th International Conference on Learning Representations (ICLR 2017) (2017)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-19835-9_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2011","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326\u2013340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_30"},{"key":"20_CR4","unstructured":"Bendisposto, J., et al.: ProB 2.0 Tutorial. In: Butler, M., Hallerstede, S., Wald\u00e9n, M. (eds.) Proceedings of the 4th Rodin User and Developer Workshop. TUCS Lecture Notes, vol. 18. TUCS (2013)"},{"key":"20_CR5","unstructured":"Bendisposto, J.M.: Directed and distributed model checking of B-Specifications. Ph.D. thesis. Universit\u00e4ts- und Landesbibliothek der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2015)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378\u2013394. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_27"},{"issue":"1\u20132","key":"20_CR7","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1017\/S1471068411000482","volume":"12","author":"M Carlsson","year":"2012","unstructured":"Carlsson, M., Mildner, P.: Sicstus prolog-the first 25 years. Theory Pract. Log. Program. 12(1\u20132), 35\u201366 (2012)","journal-title":"Theory Pract. Log. Program."},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"M Carlsson","year":"1997","unstructured":"Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191\u2013206. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0033845"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-642-28891-3_32","volume-title":"NASA Formal Methods","author":"G Chatzieleftheriou","year":"2012","unstructured":"Chatzieleftheriou, G., Bonakdarpour, B., Smolka, S.A., Katsaros, P.: Abstract model repair. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 341\u2013355. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_32"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-33600-8_11","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"J Clark","year":"2016","unstructured":"Clark, J., Bendisposto, J., Hallerstede, S., Hansen, D., Leuschel, M.: Generating Event-B specifications from algorithm descriptions. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 183\u2013197. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_11"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"20_CR12","unstructured":"ClearSy: Atelier B, User and Reference Manuals. Aix-en-Provence, France (2014). http:\/\/www.atelierb.eu\/"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 229\u2013239. ACM, New York, USA (2015)","DOI":"10.1145\/2737924.2737977"},{"key":"20_CR14","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI\/IAAI, pp. 431\u2013437. American Association for Artificial Intelligence (1998)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Gvero, T., Kuncak, V.: Interactive synthesis using free-form queries. In: Proceedings of ICSE, pp. 689\u2013692 (2015)","DOI":"10.1109\/ICSE.2015.224"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-30729-4_3","volume-title":"Integrated Formal Methods","author":"D Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA to B for Validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-30729-4_3","volume-title":"Integrated Formal Methods","author":"D Hansen","year":"2012","unstructured":"Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_3"},{"key":"20_CR18","volume-title":"Software Abstractions: Logic Language and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic Language and Analysis. MIT Press, Cambridge (2006)"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings ICSE, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-319-77935-5_18","volume-title":"NASA Formal Methods","author":"P K\u00f6rner","year":"2018","unstructured":"K\u00f6rner, P., Bendisposto, J.: Distributed model checking using ProB. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 244\u2013260. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_18"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_15"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-33693-0_23","volume-title":"Integrated Formal Methods","author":"S Krings","year":"2016","unstructured":"Krings, S., Leuschel, M.: SMT solvers for validation of B and Event-B models. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 361\u2013375. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_23"},{"key":"20_CR23","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc, Boston, MA, USA (2002)"},{"key":"20_CR24","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1002\/9781119002727.ch14","volume-title":"Formal Methods Applied to Complex Systems: Implementation of the B Method","author":"M Leuschel","year":"2014","unstructured":"Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data valiadation: the ProB constraint solver 10 years on Chapter 14. In: Boulanger, J.L. (ed.) Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 427\u2013446. Wiley ISTE, Hoboken, NJ (2014)"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"issue":"2","key":"20_CR26","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. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"11","key":"20_CR27","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/j.ipl.2016.06.003","volume":"116","author":"A Mota","year":"2016","unstructured":"Mota, A., Iyoda, J., Maranh\u00e3o, H.: Program synthesis by model finding. Inf. Process. Lett. 116(11), 701\u2013705 (2016)","journal-title":"Inf. Process. Lett."},{"key":"20_CR28","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"},{"issue":"1","key":"20_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10994-011-5259-2","volume":"86","author":"S Muggleton","year":"2012","unstructured":"Muggleton, S., Raedt, L.D., Poole, D., Bratko, I., Flach, P.A., Inoue, K., Srinivasan, A.: ILP turns 20. Mach. Learn. 86(1), 3\u201323 (2012)","journal-title":"Mach. Learn."},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Nedunuri, S., Cook, W.R., Smith, D.R.: Theory and techniques for synthesizing a family of graph algorithms. In: Proceedings First Workshop on Synthesis, EPTCS, vol. 84, pp. 33\u201346 (2012)","DOI":"10.4204\/EPTCS.84.3"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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\u00a0and Kodkod. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372\u2013386. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_31"},{"key":"20_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-319-33600-8_25","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"J Schmidt","year":"2016","unstructured":"Schmidt, J., Krings, S., Leuschel, M.: Interactive model repair by synthesis. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 303\u2013307. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_25"},{"key":"20_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"}],"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-98938-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T03:01:49Z","timestamp":1693796509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98938-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989372","9783319989389"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98938-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}