{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T18:54:53Z","timestamp":1790448893467,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544334","type":"print"},{"value":"9783662544341","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_4","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"83-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Is Your Software on Dope?"],"prefix":"10.1007","author":[{"given":"Pedro R.","family":"D\u2019Argenio","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Biewer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"4_CR1","unstructured":"Agorist, M.: WATCH: computer programmer testifies he helped rig voting machines. MintPress News (2016) http:\/\/www.mintpressnews.com\/214505-2\/214505\/. Accessed 13 Jan 2017"},{"key":"4_CR2","unstructured":"AppleInsider: Galaxy S4 on steroids: Samsung caught doping in benchmarks (2013). http:\/\/forums.appleinsider.com\/discussion\/158782\/galaxy-s-4-on-steroids-samsung-caught-doping-in-benchmarks. Accessed 13 Jan 2017"},{"issue":"394","key":"4_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.2307\/2234208","volume":"99","author":"WB Arthur","year":"1989","unstructured":"Arthur, W.B.: Competing technologies, increasing returns, and lock-in by historical events. Econ. J. 99(394), 116\u2013131 (1989). http:\/\/www.jstor.org\/stable\/2234208","journal-title":"Econ. J."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/978-3-319-47169-3_46","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"G Barthe","year":"2016","unstructured":"Barthe, G., D\u2019Argenio, P.R., Finkbeiner, B., Hermanns, H.: Facets of software doping. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 601\u2013608. Springer, Heidelberg (2016). 10.1007\/978-3-319-47169-3_46"},{"key":"4_CR6","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW-17, pp. 100\u2013114. IEEE Computer Society (2004). http:\/\/doi.ieeecomputersociety.org\/10.1109\/CSFW.2004.17"},{"issue":"6","key":"4_CR7","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. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011). http:\/\/dx.doi.org\/10.1017\/S0960129511000193","journal-title":"Math. Struct. Comput. Sci."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Arias, E.J.G., Hsu, J., Roth, A., Strub, P.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: Rajamani, S.K., Walker, D. (eds.) POPL 2015, pp. 55\u201368. ACM (2015). http:\/\/doi.acm.org\/10.1145\/2676726.2677000","DOI":"10.1145\/2775051.2677000"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1007\/978-3-319-47169-3_49","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"K Baum","year":"2016","unstructured":"Baum, K.: What the hack is wrong with software doping? In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 633\u2013647. Springer, Heidelberg (2016). 10.1007\/978-3-319-47169-3_49"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) POPL 2004, pp. 14\u201325. ACM Press (2004). http:\/\/doi.acm.org\/10.1145\/964001.964003","DOI":"10.1145\/982962.964003"},{"key":"4_CR11","unstructured":"Brignall, M.: \u2018Error 53\u2019 fury mounts as Apple software update threatens to kill your iPhone 6. The Guardian (2010). https:\/\/www.theguardian.com\/money\/2016\/feb\/05\/error-53-apple-iphone-software-update-handset-worthless-third-party-repair. Accessed 13 Jan 2017"},{"key":"4_CR12","unstructured":"Carrel, P., Bryan, V., Croft, A.: Germany asks Opel for more information in Zafira emissions probe. Reuters (2016). http:\/\/www.reuters.com\/article\/us-volkswagen-emissions-germany-opel-idUSKCN0Y92GI. Accessed 13 Jan 2017"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL 2010, pp. 57\u201370 (2010). http:\/\/doi.acm.org\/10.1145\/1706299.1706308","DOI":"10.1145\/1707801.1706308"},{"key":"4_CR14","unstructured":"Checkoway, S., Niederhagen, R., Everspaugh, A., Green, M., Lange, T., Ristenpart, T., Bernstein, D.J., Maskiewicz, J., Shacham, H., Fredrikson, M.: On the practical exploitability of dual EC in TLS implementations. In: Fu, K., Jung, J. (eds.) 23rd USENIX Security Symposium. pp. 319\u2013335. USENIX Association (2014). https:\/\/www.usenix.org\/conference\/usenixsecurity14\/technical-sessions\/presentation\/checkoway"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). 10.1007\/978-3-642-54792-8_15"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF 2008, pp. 51\u201365 (2008). http:\/\/dx.doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"issue":"6","key":"4_CR17","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). http:\/\/dx.doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"4_CR18","volume-title":"A Discipline of Programming","author":"E Dijkstra","year":"1997","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"4_CR19","unstructured":"Domke, F., Lange, D.: The exhaust emissions scandal (\u201cDieselgate\u201d). In: 30th Chaos Communication Congress (2015). https:\/\/events.ccc.de\/congress\/2015\/Fahrplan\/events\/7331.html. Accessed 13 Jan 2017"},{"key":"4_CR20","unstructured":"Dvorak, J.C.: The secret printer companies are keeping from you. PC Mag UK (2012). http:\/\/uk.pcmag.com\/printers\/60628\/opinion\/the-secret-printer-companies-are-keeping-from-you. Accessed 13 Jan 2017"},{"key":"4_CR21","unstructured":"Feldman, A.J., Halderman, J.A., Felten, E.W.: Security analysis of the Diebold AccuVote-ts voting machine. In: Martinez, R., Wagner, D. (eds.) 2007 USENIX\/ACCURATE Electronic Voting Technology Workshop, EVT 2007. USENIX Association (2007). https:\/\/www.usenix.org\/conference\/evt-07\/security-analysis-diebold-accuvote-ts-voting-machine"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: Crnkovic, I., Chechik, M., Gr\u00fcnbacher, P. (eds.) ASE 2014, pp. 349\u2013360. ACM (2014). http:\/\/doi.acm.org\/10.1145\/2642937.2642987","DOI":"10.1145\/2642937.2642987"},{"key":"4_CR23","unstructured":"Finkbeiner, B., Hahn, C.: Deciding Hyperproperties. In: Desharnais, J., Jagadeesan, R. (eds.) CONCUR 2016. LIPIcs, vol. 59, pp. 13:1\u201313:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2016\/6170"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Heidelberg (2015). 10.1007\/978-3-319-21690-4_3"},{"key":"4_CR25","unstructured":"Flak, A., Taylor, E., Wacket, M., Eckert, V., Stonestreet, J.: Test of fiat diesel model shows irregular emissions: Bild am Sonntag. Reuters (2016). http:\/\/www.reuters.com\/article\/us-fiat-emissions-germany-idUSKCN0XL0MT. Accessed 13 Jan 2017"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: Jones, N.D., Leroy, X. (eds.) POPL 2004, pp. 186\u2013197. ACM (2004). http:\/\/doi.acm.org\/10.1145\/964001.964017","DOI":"10.1145\/982962.964017"},{"issue":"3","key":"4_CR27","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1002\/stvr.1472","volume":"23","author":"B Godlin","year":"2013","unstructured":"Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Softw. Test. Verif. Reliab. 23(3), 241\u2013258 (2013)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"1","key":"4_CR28","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/MS.2016.6","volume":"33","author":"L Hatton","year":"2016","unstructured":"Hatton, L., van Genuchten, M.: When software crosses a line. IEEE Softw. 33(1), 29\u201331 (2016). http:\/\/dx.doi.org\/10.1109\/MS.2016.6","journal-title":"IEEE Softw."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) SOSP 2015, pp. 1\u201317. ACM (2015). http:\/\/doi.acm.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Lahiri, S.K., Pawar, K., Hashmi, H., Gokbulut, S., Fernando, L., Detlefs, D., Wadsworth, S.: Will you still compile me tomorrow? Static cross-version compiler validation. In: Meyer, B., Baresi, L., Mezini, M. (eds.) ESEC\/FSE 2013, pp. 191\u2013201 (2013). http:\/\/doi.acm.org\/10.1145\/2491411.2491442","DOI":"10.1145\/2491411.2491442"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, M., Seidl, H., Finkbeiner, B.: Relational abstract interpretation for the verification of 2-hypersafety properties. In: Sadeghi, A., Gligor, V.D., Yung, M. (eds.) CCS 2013, pp. 211\u2013222. ACM (2013). http:\/\/doi.acm.org\/10.1145\/2508859.2516721","DOI":"10.1145\/2508859.2516721"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2012","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712\u2013717. Springer, Heidelberg (2012). 10.1007\/978-3-642-31424-7_54"},{"key":"4_CR33","unstructured":"Manjoo, F.: Take that, stupid printer! Slate (2008). http:\/\/www.slate.com\/articles\/technology\/technology\/2008\/08\/take_that_stupid_printer.html. Accessed 13 Jan 2017"},{"key":"4_CR34","unstructured":"Margaria, T., Steffen, B. (eds.): ISoLA 2016. LNCS, vol. 9953. Springer, Heidelberg (2016)"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-41488-6_17","volume-title":"Secure IT Systems","author":"D Milushev","year":"2013","unstructured":"Milushev, D., Clarke, D.: Incremental hyperproperty model checking via games. In: Riis Nielson, H., Gollmann, D. (eds.) NordSec 2013. LNCS, vol. 8208, pp. 247\u2013262. Springer, Heidelberg (2013). 10.1007\/978-3-642-41488-6_17"},{"key":"4_CR36","unstructured":"Panzarino, M.: Apple apologizes and updates iOS to restore iPhones disabled by error 53. TechCrunch (2016). https:\/\/techcrunch.com\/2016\/02\/18\/apple-apologizes-and-updates-ios-to-restore-iphones-disabled-by-error-53\/. Accessed 13 Jan 2017"},{"key":"4_CR37","unstructured":"Schneier, B., Fredrikson, M., Kohno, T., Ristenpart, T.: Surreptitiously weakening cryptographic systems. IACR Cryptology ePrint Archive 2015, 97 (2015). http:\/\/eprint.iacr.org\/2015\/097"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Sousa, M., Dillig, I.: Cartesian Hoare logic for verifying k-safety properties. In: Krintz, C., Berger, E. (eds.) PLDI 2016, pp. 57\u201369. ACM (2016). http:\/\/doi.acm.org\/10.1145\/2908080.2908092","DOI":"10.1145\/2980983.2908092"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). 10.1007\/11547662_24"},{"key":"4_CR40","unstructured":"Tritech Computer Solutions: Dell laptops reject third-party batteries and AC adapters\/chargers. Hardware vendor lock-in? https:\/\/nctritech.wordpress.com\/2010\/01\/26\/dell-laptops-reject-third-party-batteries-and-ac-adapterschargers-hardware-vendor-lock-in\/ (2010). Accessed 13 Jan 2017"},{"key":"4_CR41","unstructured":"Waller, K.: Has a printer update rendered your cartridges redundant? Which? (2016). https:\/\/conversation.which.co.uk\/technology\/printer-software-update-third-party-printer-ink\/. Accessed 13 Jan 2017"},{"key":"4_CR42","unstructured":"Waste Ink: Epson firmware update = no to compatibles. http:\/\/www.wasteink.co.uk\/epson-firmware-update-compatible-problem\/ (2012). Accessed 13 Jan 2017"},{"key":"4_CR43","unstructured":"Wikipedia: Volkswagen emissions scandal. Wikipedia, The Free Encyclopedia (2016). https:\/\/en.wikipedia.org\/wiki\/Volkswagen_emissions_scandal. Accessed 13 Jan 2017"},{"issue":"1\u20133","key":"4_CR44","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. Theor. Comput. Sci. 375(1\u20133), 308\u2013334 (2007). http:\/\/dx.doi.org\/10.1016\/j.tcs.2006.12.036","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54434-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T15:39:13Z","timestamp":1635262753000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_4"}},"subtitle":["Formal Analysis of Surreptitiously \u201cenhanced\u201d Programs"],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}