{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T08:21:47Z","timestamp":1782289307150,"version":"3.54.5"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319929934","type":"print"},{"value":"9783319929941","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-92994-1_3","type":"book-chapter","created":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T06:48:51Z","timestamp":1527835731000},"page":"44-62","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Static and Dynamic Verification of Relational Properties on Self-composed C Code"],"prefix":"10.1007","author":[{"given":"Lionel","family":"Blatter","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1557-2813","authenticated-orcid":false,"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7203-0968","authenticated-orcid":false,"given":"Virgile","family":"Prevosto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guillaume","family":"Petiot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,6,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: Proceedings of the 38th SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), pp. 362\u2013375. ACM (2017)","DOI":"10.1145\/3062341.3062378"},{"issue":"5","key":"3_CR2","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1016\/j.jlamp.2016.05.004","volume":"85","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Log. Algebr. Methods Program. 85(5), 847\u2013859 (2016)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"6","key":"3_CR3","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. J. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011)","journal-title":"J. Math. Struct. Comput. Sci."},{"key":"3_CR4","unstructured":"Baudin, P., Bobot, F., Correnson, L., Dargaye, Z.: WP Plugin Manual v1.0 (2017). \nhttp:\/\/frama-c.com\/download\/frama-c-wp-manual.pdf"},{"key":"3_CR5","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language. \nhttp:\/\/frama-c.com\/acsl.html"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 14\u201325 (2004)","DOI":"10.1145\/964001.964003"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Bishop, P.G., Bloomfield, R.E., Cyra, L.: Combining testing and proof to gain high assurance in software: a case study. In: 24th International Symposium on Software Reliability Engineering (ISSRE 2013), pp. 248\u2013257. IEEE (2013)","DOI":"10.1109\/ISSRE.2013.6698924"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-662-54577-5_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Blatter","year":"2017","unstructured":"Blatter, L., Kosmatov, N., Le Gall, P., Prevosto, V.: RPP: automatic proof of relational properties by self-composition. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 391\u2013397. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_22"},{"issue":"5","key":"3_CR9","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/s10009-011-0192-z","volume":"13","author":"P Cuoq","year":"2011","unstructured":"Cuoq, P., Monate, B., Pacalet, A., Prevosto, V.: Functional dependencies of C functions via weakest pre-conditions. Int. J. Softw. Tools Technol. Transf. (STTT) 13(5), 405\u2013417 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Proceedings of the ACM Symposium on Applied Computing (SAC 2013), pp. 1230\u20131235. ACM (2013)","DOI":"10.1145\/2480362.2480593"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics, vol. 19 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"3_CR12","doi-asserted-by":"publisher","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"},{"issue":"3","key":"3_CR13","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-017-9433-5","volume":"60","author":"M Kiefer","year":"2018","unstructured":"Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR - combining static verification and dynamic analysis. J. Autom. Reason. 60(3), 337\u2013363 (2018)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"3_CR14","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 Asp. Comput. 27(3), 573\u2013609 (2015). \nhttp:\/\/frama-c.com","journal-title":"Formal Asp. Comput."},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-54108-7_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"KRM Leino","year":"2014","unstructured":"Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 170\u2013190. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54108-7_9"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Petiot, G., Botella, B., Julliand, J., Kosmatov, N., Signoles, J.: Instrumentation of annotated C programs for test generation. In: 14th International Working Conference on Source Code Analysis and Manipulation (SCAM 2014), pp. 105\u2013114. IEEE (2014)","DOI":"10.1109\/SCAM.2014.19"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-41135-4_8","volume-title":"Tests and Proofs","author":"G Petiot","year":"2016","unstructured":"Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., Julliand, J.: Your proof fails? Testing helps to find the reason. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 130\u2013150. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41135-4_8"},{"key":"3_CR18","unstructured":"Signoles, J.: E-ACSL: Executable ANSI\/ISO C Specification Language (2012). \nhttp:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), pp. 57\u201369. ACM (2016)","DOI":"10.1145\/2908080.2908092"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Vorobyov, K., Signoles, J., Kosmatov, N.: Shadow state encoding for efficient monitoring of block-level properties. In: Proceedings of the International Symposium on Memory Management (ISMM 2017), pp. 47\u201358. ACM (2017)","DOI":"10.1145\/3092255.3092269"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92994-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,1]],"date-time":"2018-06-01T06:50:49Z","timestamp":1527835849000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92994-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929934","9783319929941"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92994-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}