{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T04:01:41Z","timestamp":1775880101378,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415901","type":"print"},{"value":"9783319415918","type":"electronic"}],"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-41591-8_24","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T17:27:27Z","timestamp":1466702847000},"page":"347-366","source":"Crossref","is-referenced-by-count":29,"title":["CoCoSpec: A Mode-Aware Contract Language for Reactive Systems"],"prefix":"10.1007","author":[{"given":"Adrien","family":"Champion","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-17524-9_7","volume-title":"NASA Formal Methods","author":"J Backes","year":"2015","unstructured":"Backes, J., Cofer, D., Miller, S., Whalen, M.W.: Requirements analysis of a quad-redundant flight control system. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 82\u201396. Springer, Heidelberg (2015)"},{"key":"24_CR2","volume-title":"High Integrity Software - The SPARK Approach to Safety and Security","author":"JGP Barnes","year":"2003","unstructured":"Barnes, J.G.P.: High Integrity Software - The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M Gheorghiu Bobaru","year":"2008","unstructured":"Gheorghiu Bobaru, M., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135\u2013148. Springer, Heidelberg (2008)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-319-19249-9_20","volume-title":"FM 2015: Formal Methods","author":"G Brat","year":"2015","unstructured":"Brat, G., Bushnell, D., Davies, M., Giannakopoulou, D., Howar, F., Kahsai, T.: Verifying the safety of a flight-critical system. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 308\u2013324. Springer, Heidelberg (2015)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780. Springer International Publishing, Switzerland (2016, to appear)","DOI":"10.1007\/978-3-319-41540-6_29"},{"issue":"4","key":"24_CR6","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/2377656.2377659","volume":"21","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Validation of requirements for hybrid systems: a formal approach. ACM Trans. Softw. Eng. Methodol. 21(4), 22 (2012)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: Cortellessa, V., Muccini, H., Demir\u00f6rs, O. (eds.) 38th Euromicro Conference on Software Engineering and Advanced Applications, SEAA 2012. IEEE Computer Society (2012)","DOI":"10.1109\/SEAA.2012.68"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Dieumegard, A., Garoche, P., Kahsai, T., Taillar, A., Thirioux, X.: Compilation of synchronous observers as code contracts. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015. ACM (2015)","DOI":"10.1145\/2695664.2695819"},{"key":"24_CR10","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"24_CR11","unstructured":"Halbwachs, N., Fernandez, J.C., Bouajjanni, A.: An executable temporal logic to express safety properties and its connection with the language lustre. In: Sixth International Symposium on Lucid and Intensional Programming, ISLIP 1993 (1993)"},{"issue":"9","key":"24_CR12","doi-asserted-by":"crossref","first-page":"785","DOI":"10.1109\/32.159839","volume":"18","author":"N Halbwachs","year":"1992","unstructured":"Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. IEEE Trans. Software Eng. 18(9), 785\u2013793 (1992)","journal-title":"IEEE Trans. Software Eng."},{"key":"24_CR13","series-title":"Workshops in Computing","first-page":"83","volume-title":"Algebraic Methodology and Software Technology (AMAST): Proceedings of the Third International Conference on Methodology and Software Technology, 1993","author":"N Halbwachs","year":"1993","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Nivat, M., Rattray, C., Rus, T., Scollo, G. (eds.) Algebraic Methodology and Software Technology (AMAST). Workshops in Computing, pp. 83\u201396. Springer, London (1993)"},{"issue":"10","key":"24_CR14","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"24_CR15","unstructured":"Hueschen, R.M.: Development of the Transport Class Model (TCM) aircraft simulation from a sub-scale Generic Transport Model (GTM) simulation. Technical report, NASA, Langley Research Center (2011)"},{"issue":"1","key":"24_CR16","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1109\/2.562936","volume":"30","author":"J J\u00e9z\u00e9quel","year":"1997","unstructured":"J\u00e9z\u00e9quel, J., Meyer, B.: Design by contract: the lessons of Ariane. IEEE Comput. 30(1), 129\u2013130 (1997)","journal-title":"IEEE Comput."},{"key":"24_CR17","unstructured":"Jones, C.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University (1981)"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Barnat, J., Heljanko, K. (eds.) Proceedings 10th International Workshop on Parallel and Distributed Methods in VerifiCation, PDMC 2011. EPTCS, vol. 72 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"24_CR19","unstructured":"Kamp, J.: Tense logic and the theory of order. Ph.D. Thesis, UCLA (1968)"},{"issue":"3","key":"24_CR20","doi-asserted-by":"crossref","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. Form. Asp. Comput. 27(3), 573\u2013609 (2015)","journal-title":"Form. Asp. Comput."},{"key":"24_CR21","series-title":"The Springer International Series in Engineering and Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"GT Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. The Springer International Series in Engineering and Computer Science, vol. 523, pp. 175\u2013188. Springer, New York (1999)"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"24_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995)"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 342\u2013346. Springer, Heidelberg (1999)"},{"issue":"10","key":"24_CR25","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Comput. 25(10), 40\u201351 (1992)","journal-title":"IEEE Comput."},{"key":"24_CR26","unstructured":"Parnas, D.L.: Inspection of safety-critical software using program-function tables. In: Duncan, K.A., Krueger, K.H. (eds.) Linkage and Developing Countries, Information Processing, 1994, IFIP Transactions, vol. A-53. North-Holland (1994)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T03:25:00Z","timestamp":1568085900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}