{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:48:57Z","timestamp":1742914137339,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031753794"},{"type":"electronic","value":"9783031753800"}],"license":[{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75380-0_6","type":"book-chapter","created":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T08:29:02Z","timestamp":1730190542000},"page":"79-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Contract-LIB: A Proposal for\u00a0a\u00a0Common Interchange Format for\u00a0Software System Specification"],"prefix":"10.1007","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[]},{"given":"Wolfram","family":"Pfeifer","sequence":"additional","affiliation":[]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,30]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","author":"J Abrial","year":"1996","unstructured":"Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (1996). https:\/\/doi.org\/10.1017\/CBO9780511624162","journal-title":"Cambridge University Press"},{"issue":"6","key":"6_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447\u2013466 (2010)","journal-title":"STTT"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification \u2013 The KeY Book, LNCS, vol. 10001. Springer (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"6_CR4","unstructured":"Ameri, M., Furia, C.A.: Why just boogie? translating between intermediate verification languages. CoRR abs\/1601.00516 (2016). http:\/\/arxiv.org\/abs\/1601.00516"},{"key":"6_CR5","unstructured":"Aravantinos, V., Voss, S., Teufl, S., H\u00f6lzl, F., Sch\u00e4tz, B.: Autofocus 3: tooling concepts for seamless, model-based development of embedded systems. ACES-MB &WUCOR@ MoDELS 1508, 19\u201326 (2015)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Armborst, L., et al.: The vercors verifier: a progress report. In: Computer Aided Verification (CAV) 2024 (2024), to appear","DOI":"10.1007\/978-3-031-65630-9_1"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Armborst, L., Lathouwers, S., Huisman, M.: Joining forces! reusing contracts for deductive verifiers through automatic translation. In: International Conference on Integrated Formal Methods, pp. 153\u2013171. Springer (2023)","DOI":"10.1007\/978-3-031-47705-8_9"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Astesiano, E., et al.: CASL: the common algebraic specification language. Theoret. Comput. Sci. 286(2), 153\u2013196 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00368-1. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397501003681","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de\u00a0Boer, F.S., Bonsangue, M.M., Graf, S., de\u00a0Roever, W.P. (eds.) Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures. Lecture Notes in Computer Science, vol.\u00a04111, pp. 364\u2013387. Springer, Cham (2005). https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"6_CR11","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MSEC.2022.3154689","volume":"20","author":"D Basin","year":"2022","unstructured":"Basin, D., Cremers, C., Dreier, J., Sasse, R.: Tamarin: verification of large-scale, real-world, cryptographic protocols. IEEE Secur. Privacy 20(3), 24\u201332 (2022)","journal-title":"IEEE Secur. Privacy"},{"key":"6_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Proc. TACAS\u00a0(3). LNCS, vol. 14572, pp. 299\u2013329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"6_CR14","unstructured":"Bhargavan, K., et\u00a0al.: Everest: towards a verified, drop-in replacement of https. In: 2nd Summit on Advances in Programming Languages (2017)"},{"key":"6_CR15","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroc\u0142aw, Poland (August 2011)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/11559306_15","volume-title":"Frontiers of Combining Systems","author":"E B\u00f6rger","year":"2005","unstructured":"B\u00f6rger, E.: The ASM method for system design and analysis. A tutorial introduction. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 264\u2013283. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_15"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102\u2013126. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722010_8"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Tip: tons of inductive problems. In: International Conference on Intelligent Computer Mathematics, pp. 333\u2013337. Springer (2015)","DOI":"10.1007\/978-3-319-20615-8_23"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Cok, D.R.: Openjml: Software verification for java 7 using jml, openjdk, and eclipse. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014. EPTCS, vol.\u00a0149, pp. 79\u201392 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.8","DOI":"10.4204\/EPTCS.149.8"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-030-17502-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ernst","year":"2019","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis \u2013 verification competition with a human factor. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 176\u2013195. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_12"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-030-25543-5_13","volume-title":"Computer Aided Verification","author":"G Ernst","year":"2019","unstructured":"Ernst, G., Murray, T.: SecCSL: Security Concurrent Separation Logic. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 208\u2013230. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_13"},{"issue":"6","key":"6_CR22","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: Kiv: overview and verifythis competition. Int. J. Softw. Tools Technol. Transfer 17(6), 677\u2013694 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0308-3","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Ernst, G., Weigl, A.: Verify this: Memcached-a practical long-term challenge for the integration of formal methods. In: International Conference on Integrated Formal Methods, pp. 82\u201389. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_5","DOI":"10.1007\/978-3-031-47705-8_5"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Tiwari, A.: Challenges of multilingual program specification and analysis. In: ISoLA 2024. LNCS. Springer (2024)","DOI":"10.1007\/978-3-031-75380-0_8"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-662-48899-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T Gauthier","year":"2015","unstructured":"Gauthier, T., Kaliszyk, C.: Sharing HOL4 and HOL light proof knowledge. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 372\u2013386. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_26"},{"key":"6_CR27","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-031-38828-6_6","volume-title":"Tests and Proofs","author":"M Gogolla","year":"2023","unstructured":"Gogolla, M., Hamann, L.: Proving properties of operation contracts with test scenarios. In: Prevosto, V., Seceleanu, C. (eds.) Tests and Proofs, pp. 97\u2013107. Springer, Cham (2023)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. Computing and Software Science: State of the Art and Perspectives, pp. 345\u2013373 (2019)","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-030-64354-6_10","volume-title":"Deductive Software Verification: Future Perspectives","author":"M Huisman","year":"2020","unstructured":"Huisman, M., Monti, R., Ulbrich, M., Weigl, A.: The VerifyThis collaborative long term challenge. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 246\u2013260. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_10"},{"issue":"2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002). https:\/\/doi.org\/10.1145\/505145.505149","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"issue":"3","key":"6_CR32","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/S00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267\u2013288 (2011). https:\/\/doi.org\/10.1007\/S00165-010-0152-5","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"6_CR33","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/S00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/S00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"6_CR34","doi-asserted-by":"publisher","unstructured":"Klamroth, J., Lanzinger, F., Pfeifer, W., Ulbrich, M.: The Karlsruhe Java verification suite. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds.) The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13360, pp. 290\u2013312. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-08166-8_14","DOI":"10.1007\/978-3-031-08166-8_14"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"M.\u00a0Leino, K.R.: Accessible software verification with dafny. IEEE Softw. 34(6), 94\u201397 (2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","DOI":"10.1109\/MS.2017.4121212"},{"issue":"10","key":"6_CR36","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u2019\u2019. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"6_CR37","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a050, pp. 104\u2013125. IOS Press (2017). https:\/\/doi.org\/10.3233\/978-1-61499-810-5-104","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2 , btormc and boolector 3.0. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 587\u2013595. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"de\u00a0Roever, W.P., Engelhardt, K.: Data Refinement: Model-oriented Proof Theories and their Comparison, Cambridge Tracts in Theoretical Computer Science, vol.\u00a046. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., et al.: Moxi: an intermediate language for symbolic model. In: SPIN (2024)","DOI":"10.1007\/978-3-031-66149-5_2"},{"key":"6_CR41","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: Stepping Stones in the TPTP World. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Proceedings of the 12th International Joint Conference on Automated Reasoning. p. To appear. Lecture Notes in Artificial Intelligence (2024)","DOI":"10.1007\/978-3-031-63498-7_3"},{"key":"6_CR42","unstructured":"Thir\u00e9, F.: Interoperability between proof systems using the logical framework Dedukti. Ph.D. thesis, Universit\u00e9 Paris-Saclay (2020)"},{"key":"6_CR43","doi-asserted-by":"publisher","unstructured":"Vakili, A., Day, N.A.: Avestan: A declarative modeling language based on smt-lib. In: 2012 4th International Workshop on Modeling in Software Engineering (MISE), pp. 36\u201342 (2012). https:\/\/doi.org\/10.1109\/MISE.2012.6226012","DOI":"10.1109\/MISE.2012.6226012"},{"key":"6_CR44","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z - specification, refinement, and proof. Prentice Hall international series in computer science, Prentice Hall (1996)"},{"key":"6_CR45","unstructured":"Xu, M.: Research Report: Not All Move Specifications Are Created Equal. In: Proceedings of the 2024 Workshop on Language-Theoretic Security (LangSec). San Francisco, CA, May 2024"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75380-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,30]],"date-time":"2024-11-30T12:05:09Z","timestamp":1732968309000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75380-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,30]]},"ISBN":["9783031753794","9783031753800"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75380-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,30]]},"assertion":[{"value":"30 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}