{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:42:49Z","timestamp":1743100969710,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"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-47166-2_58","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"839-855","source":"Crossref","is-referenced-by-count":3,"title":["Proof-Carrying Apps: Contract-Based Deployment-Time Verification"],"prefix":"10.1007","author":[{"given":"S\u00f6nke","family":"Holthusen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Nieke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"58_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"W Ahrendt","year":"2014","unstructured":"Ahrendt, W., et al.: The KeY platform for verification and analysis of Java Programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Heidelberg (2014). http:\/\/dx.doi.org\/10.1007\/978-3-319-12154-3_4"},{"key":"58_CR2","doi-asserted-by":"crossref","unstructured":"Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the saturn project. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE 2007, pp. 43\u201348. ACM, New York (2007). http:\/\/doi.acm.org\/10.1145\/1251535.1251543","DOI":"10.1145\/1251535.1251543"},{"key":"58_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-37521-7","volume-title":"Feature-Oriented Software Product Lines: Concepts and Implementation","author":"S Apel","year":"2013","unstructured":"Apel, S., Batory, D., K\u00e4stner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer, Heidelberg (2013)"},{"key":"58_CR4","doi-asserted-by":"crossref","unstructured":"Arzt, S., Bodden, E.: Reviser: efficiently updating IDE-\/IFDS-based data-flow analyses in response to incremental program changes. In: International Conference on Software Engineering, ICSE 2014, pp. 288\u2013298. ACM, New York (2014). http:\/\/doi.acm.org\/10.1145\/2568225.2568243","DOI":"10.1145\/2568225.2568243"},{"key":"58_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"58_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-92188-2_1","volume-title":"Formal Methods for Components and Objects","author":"G Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 1\u201324. Springer, Heidelberg (2008). http:\/\/dx.doi.org\/10.1007\/978-3-540-92188-2_1"},{"key":"58_CR7","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). http:\/\/dx.doi.org\/10.1007\/978-3-662-07964-5"},{"key":"58_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Qadeer, S., Gopalakrishnan, G. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). http:\/\/dx.doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"58_CR9","doi-asserted-by":"crossref","unstructured":"Brat, G., Visser, W.: Combining static analysis and model checking for software analysis. In: International Conference on Automated Software Engineering, ASE 2001, p. 262. IEEE Computer Society, Washington (2001). http:\/\/dl.acm.org\/citation.cfm?id=872023.872568","DOI":"10.1109\/ASE.2001.989812"},{"key":"58_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/978-3-662-45231-8_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"R Bubel","year":"2014","unstructured":"Bubel, R., H\u00e4hnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 120\u2013134. Springer, Heidelberg (2014). http:\/\/dx.doi.org\/10.1007\/978-3-662-45231-8_9"},{"key":"58_CR11","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Lam, M.S. (ed.) Conference on Programming Language Design and Implementation, pp. 95\u2013107. ACM (2000). http:\/\/doi.acm.org\/10.1145\/349299.349315","DOI":"10.1145\/358438.349315"},{"key":"58_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/978-3-642-38574-2_21","volume-title":"Automated Deduction \u2013 CADE-24","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 300\u2013314. Springer, Heidelberg (2013). http:\/\/dx.doi.org\/10.1007\/978-3-642-38574-2_21"},{"issue":"3","key":"58_CR13","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16 (2012). http:\/\/doi.acm.org\/10.1145\/2187671.2187678","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"58_CR14","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000). http:\/\/dx.doi.org\/10.1007\/s100090050043","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"58_CR15","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. (CSUR) 41(4), 21 (2009)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"58_CR16","unstructured":"Lam, P., Bodden, E., Lhot\u00e1k, O., Hendren, L.: The Soot framework for Java program analysis: a retrospective (2011)"},{"key":"58_CR17","doi-asserted-by":"crossref","unstructured":"Lauterburg, S., Sobeih, A., Marinov, D., Viswanathan, M.: Incremental state-space exploration for programs with dynamically allocated data. In: International Conference on Software Engineering, ICSE 2008, pp. 291\u2013300. ACM, New York (2008). http:\/\/doi.acm.org\/10.1145\/1368088.1368128","DOI":"10.1145\/1368088.1368128"},{"key":"58_CR18","unstructured":"Leavens, G.T.: JML: expressive contracts, specification inheritance, and behavioral subtyping. In: Principles and Practices of Programming on the Java Platform, p. 1 (2015). http:\/\/doi.acm.org\/10.1145\/2807426.2817926"},{"key":"58_CR19","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348\u2013370 (2010). http:\/\/dx.doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"issue":"10","key":"58_CR20","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). http:\/\/doi.ieeecomputersociety.org\/10.1109\/2.161279","journal-title":"IEEE Comput."},{"key":"58_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-642-54804-8_9","volume-title":"Fundamental Approaches to Software Engineering","author":"R Mudduluru","year":"2014","unstructured":"Mudduluru, R., Ramanathan, M.K.: Efficient incremental static analysis using path abstraction. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 125\u2013139. Springer, Heidelberg (2014). http:\/\/dx.doi.org\/10.1007\/978-3-642-54804-8_9"},{"key":"58_CR22","unstructured":"Necula, G.C.: Proof-carrying code. In: Lee, P., Henglein, F., Jones, N.D. (eds.) Symposium on Principles of Programming Languages, pp. 106\u2013119. ACM Press (1997). http:\/\/doi.acm.org\/10.1145\/263699.263712"},{"key":"58_CR23","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Davidson, J.W., Cooper, K.D., Berman, A.M. (eds.) Conference on Programming Language Design and Implementation, pp. 333\u2013344. ACM (1998). http:\/\/doi.acm.org\/10.1145\/277650.277752"},{"key":"58_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). http:\/\/dx.doi.org\/10.1007\/978-3-662-03811-6"},{"key":"58_CR25","doi-asserted-by":"crossref","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: Conference on Programming Language Design and Implementation, PLDI 2011, pp. 504\u2013515. ACM, New York (2011). http:\/\/doi.acm.org\/10.1145\/1993498.1993558","DOI":"10.1145\/1993498.1993558"},{"issue":"5","key":"58_CR26","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1067627.806586","volume":"15","author":"JM Rushby","year":"1981","unstructured":"Rushby, J.M.: Design and verification of secure systems. SIGOPS Oper. Syst. Rev. 15(5), 12\u201321 (1981). http:\/\/doi.acm.org\/10.1145\/1067627.806586","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"58_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-22646-9","volume-title":"Automated Theorem Proving in Software Engineering","author":"JM Schumann","year":"2001","unstructured":"Schumann, J.M.: Automated Theorem Proving in Software Engineering. Springer, Heidelberg (2001)"},{"issue":"1","key":"58_CR28","doi-asserted-by":"crossref","first-page":"6:1","DOI":"10.1145\/2580950","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm, T., Apel, S., K\u00e4stner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6:1\u20136:45 (2014). http:\/\/doi.acm.org\/10.1145\/2580950","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_58","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:22:08Z","timestamp":1498335728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}