{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:07:39Z","timestamp":1743059259325,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031552472"},{"type":"electronic","value":"9783031552489"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-55248-9_3","type":"book-chapter","created":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T11:02:20Z","timestamp":1710500540000},"page":"56-81","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Automatically Verified Prototype of\u00a0a\u00a0Landing Gear System"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6970-8790","authenticated-orcid":false,"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,3,16]]},"reference":[{"key":"3_CR1","unstructured":"AnimB: B model animator. http:\/\/www.animb.org\/"},{"key":"3_CR2","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 (1996)"},{"key":"3_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","DOI":"10.1007\/s10009-010-0145-y"},{"key":"3_CR5","series-title":"CCIS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07512-9_1","volume-title":"ABZ 2014","author":"F Boniol","year":"2014","unstructured":"Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1\u201318. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_1"},{"key":"3_CR6","volume-title":"Computable Set Theory","author":"D Cantone","year":"1989","unstructured":"Cantone, D., Ferro, A., Omodeo, E.: Computable Set Theory. Clarendon Press, USA (1989)"},{"issue":"7","key":"3_CR7","doi-asserted-by":"publisher","first-page":"1891","DOI":"10.1093\/comjnl\/bxab030","volume":"65","author":"M Cristi\u00e1","year":"2022","unstructured":"Cristi\u00e1, M., Katz, R.D., Rossi, G.: Proof automation in the theory of finite sets and finite set relation algebra. Comput. J. 65(7), 1891\u20131903 (2022). https:\/\/doi.org\/10.1093\/comjnl\/bxab030","journal-title":"Comput. J."},{"key":"3_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-030-02149-8_20","volume-title":"Relational and Algebraic Methods in Computer Science","author":"M Cristi\u00e1","year":"2018","unstructured":"Cristi\u00e1, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) RAMiCS 2018. LNCS, vol. 11194, pp. 333\u2013349. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02149-8_20"},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","volume":"64","author":"M Cristi\u00e1","year":"2020","unstructured":"Cristi\u00e1, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64(2), 295\u2013330 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09520-4","journal-title":"J. Autom. Reason."},{"issue":"4","key":"3_CR10","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10817-020-09577-6","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated proof of Bell-LaPadula security properties. J. Autom. Reason. 65(4), 463\u2013478 (2021). https:\/\/doi.org\/10.1007\/s10817-020-09577-6","journal-title":"J. Autom. Reason."},{"issue":"6","key":"3_CR11","doi-asserted-by":"publisher","first-page":"809","DOI":"10.1007\/s10817-021-09589-w","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated reasoning with restricted intensional sets. J. Autom. Reason. 65(6), 809\u2013890 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09589-w","journal-title":"J. Autom. Reason."},{"issue":"8","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1125","DOI":"10.1007\/s10817-021-09602-2","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: An automatically verified prototype of the Tokeneer ID station specification. J. Autom. Reason. 65(8), 1125\u20131151 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09602-2","journal-title":"J. Autom. Reason."},{"key":"3_CR13","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for a theory of finite sets with finite integer intervals. CoRR abs\/2105.03005 (2021). https:\/\/arxiv.org\/abs\/2105.03005"},{"key":"3_CR14","unstructured":"Cristi\u00e1, M., Rossi, G.: $$\\{log\\}$$: applications to software specification, prototyping and verification. CoRR abs\/2103.14933 (2021). https:\/\/arxiv.org\/abs\/2103.14933"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1017\/S1471068421000521","volume":"23","author":"M Cristi\u00e1","year":"2023","unstructured":"Cristi\u00e1, M., Rossi, G.: Integrating cardinality constraints into constraint logic programming with sets. Theory Pract. Log. Program. 23(2), 468\u2013502 (2023). https:\/\/doi.org\/10.1017\/S1471068421000521","journal-title":"Theory Pract. Log. Program."},{"key":"3_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-40561-7_16","volume-title":"SEFM 2013","author":"M Cristi\u00e1","year":"2013","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: $$\\{log\\}$$ as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 229\u2013243. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40561-7_16"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0743-1066(95)00147-6","volume":"28","author":"A Dovier","year":"1996","unstructured":"Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: A language for programming in logic with finite sets. J. Log. Program. 28(1), 1\u201344 (1996). https:\/\/doi.org\/10.1016\/0743-1066(95)00147-6","journal-title":"J. Log. Program."},{"issue":"5","key":"3_CR18","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"3_CR19","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log Program. 6(6), 645\u2013701 (2006). https:\/\/doi.org\/10.1017\/S1471068406002730","journal-title":"Theory Pract. Log Program."},{"key":"3_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-61551-2_76","volume-title":"CP 1996","author":"C Holzbaur","year":"1996","unstructured":"Holzbaur, C., Menezes, F., Barahona, P.: Defeasibility in CLP(Q) through generalized slack variables. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 209\u2013223. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61551-2_76"},{"issue":"1\u20133","key":"3_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0743-1066(98)10002-X","volume":"37","author":"J Jaffar","year":"1998","unstructured":"Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The semantics of constraint logic programs. J. Log. Program. 37(1\u20133), 1\u201346 (1998). https:\/\/doi.org\/10.1016\/S0743-1066(98)10002-X","journal-title":"J. Log. Program."},{"issue":"3","key":"3_CR22","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1145\/319301.319317","volume":"21","author":"L Lamport","year":"1999","unstructured":"Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Trans. Program. Lang. Syst. 21(3), 502\u2013526 (1999). https:\/\/doi.org\/10.1145\/319301.319317","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Keijiro, A., 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"},{"key":"3_CR24","series-title":"CCIS","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-319-07512-9_6","volume-title":"ABZ 2014","author":"A Mammar","year":"2014","unstructured":"Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K. (eds.) ABZ 2014. CCIS, vol. 433, pp. 80\u201394. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-07512-9_6"},{"issue":"2","key":"3_CR25","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-015-0391-0","volume":"19","author":"A Mammar","year":"2017","unstructured":"Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. Int. J. Softw. Tools Technol. Transf. 19(2), 167\u2013186 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0391-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR26","unstructured":"Rossi, G.: $$\\{log\\}$$ (2008). http:\/\/www.clpset.unipr.it\/setlog.Home.html. Accessed 2022"},{"key":"3_CR27","unstructured":"Rossi, G., Cristi\u00e1, M.: $$\\{log\\}$$ user\u2019s manual. Technical report, Dipartimento di Matematica, Universit\u00e1 di Parma (2020). http:\/\/www.clpset.unipr.it\/SETLOG\/setlog-man.pdf"},{"key":"3_CR28","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9575-1","volume-title":"Programming with Sets - An Introduction to SETL","author":"JT Schwartz","year":"1986","unstructured":"Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets - An Introduction to SETL. Texts and Monographs in Computer Science, Springer, New York (1986). https:\/\/doi.org\/10.1007\/978-1-4613-9575-1"},{"key":"3_CR29","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)"}],"container-title":["Lecture Notes in Computer Science","From Computational Logic to Computational Biology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-55248-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,15]],"date-time":"2024-03-15T11:02:32Z","timestamp":1710500552000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-55248-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031552472","9783031552489"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-55248-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"16 March 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}