{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:22Z","timestamp":1725516502096},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_13","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"105-115","source":"Crossref","is-referenced-by-count":0,"title":["Modular Reasoning in Object-Oriented Programming"],"prefix":"10.1007","author":[{"given":"David A.","family":"Naumann","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: ACM Symp. on Princ. of Program. Lang. (POPL) (1999)","DOI":"10.1145\/292540.292555"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24851-4_1","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"J. Aldrich","year":"2004","unstructured":"Aldrich, J., Chambers, C.: Ownership Domains: Separating Aliasing Policy from Mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 1\u201325. Springer, Heidelberg (2004)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: POPL (2006), Extended version available as KSU CIS-TR-2005-1","DOI":"10.1145\/1111037.1111046"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45500-0_21","volume-title":"Theoretical Aspects of Computer Software","author":"A. Banerjee","year":"2001","unstructured":"Banerjee, A., Heintze, N., Riecke, J.G.: Design and correctness of program transformations based on control-flow analysis. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 420\u2013447. Springer, Heidelberg (2001)"},{"issue":"6","key":"13_CR5","doi-asserted-by":"publisher","first-page":"894","DOI":"10.1145\/1101821.1101824","volume":"52","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM\u00a052(6), 894\u2013960 (2005)","journal-title":"Journal of the ACM"},{"issue":"2","key":"13_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Stack-based access control for secure information flow. Journal of Functional Programming\u00a015(2), 131\u2013177 (2005)","journal-title":"Journal of Functional Programming"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/11531142_17","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: State Based Ownership, Reentrance, and Encapsulation. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 387\u2013411. Springer, Heidelberg (2005)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","first-page":"27","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"M. Barnett","year":"2003","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 27\u201356. Springer, Heidelberg (2003); Journal of Object Technology, 3(6), 27\u201356, (2004)"},{"key":"13_CR9","unstructured":"Barnett, M., DeLine, R., Jacobs, B., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: Challenges and directions. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends Need a Bit More: Maintaining Invariants Over Shared State. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 54\u201384. Springer, Heidelberg (2004)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW 2004), pp. 100\u2013114 (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: ACM Symp. on Princ. of Program. Lang. (POPL), pp. 14\u201325 (2004)","DOI":"10.1145\/964001.964003"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Bierman, G., Parkinson, M.: Separation logic and abstraction. In: ACM Symp. on Princ. of Program. Lang (POPL), pp. 247\u2013258 (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: IEEE Symp. on Logic in Computer Science (LICS), pp. 260\u2013269 (2005)","DOI":"10.1109\/LICS.2005.47"},{"issue":"1-3","key":"13_CR16","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.03.003","volume":"52","author":"P. Borba","year":"2004","unstructured":"Borba, P., Sampaio, A., Cavalcanti, A., Corn\u00e9lio, M.: Algebraic reasoning for object-oriented programming. Sci. Comput. Programming\u00a052(1-3), 53\u2013100 (2004)","journal-title":"Sci. Comput. Programming"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45614-7_27","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"A.L.C. Cavalcanti","year":"2002","unstructured":"Cavalcanti, A.L.C., Naumann, D.A.: Forward Simulation for Data Refinement of Classes. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 471\u2013490. Springer, Heidelberg (2002)"},{"key":"13_CR18","unstructured":"Clarke, D.: Object ownership and containment. In: Dissertation, Computer Science and Engineering, University of New South Wales, Australia (2001)"},{"key":"13_CR19","unstructured":"DeLine, R., F\u00e4hndrich, M.: The Fugue protocol checker: Is your software baroque (2003), http:\/\/research.microsoft.com\/~maf\/papers.html"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1109\/ICSE.1996.493421","volume-title":"Proceedings of the 18th International Conference on Software Engineering","author":"K.K. Dhara","year":"1996","unstructured":"Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, March 1996, pp. 258\u2013267. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"13_CR21","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"13_CR22","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"13_CR23","volume-title":"Program Design Calculi","author":"D. Gries","year":"1993","unstructured":"Gries, D.: Data refinement and the tranform. In: Broy, M. (ed.) Program Design Calculi, International Summer School at Marktoberdorf, Springer, Heidelberg (1993)"},{"key":"13_CR24","unstructured":"Hoare, T., Misra, J.: Verified software: Theories, tools, experiments. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"I.T. Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Prog. Lang. Syst (2006)","DOI":"10.1145\/1146809.1146811"},{"key":"13_CR27","unstructured":"Leavens, G.T., Clifton, C.: Lessons from the JML project. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object Invariants in Dynamic Contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013515. Springer, Heidelberg (2004)"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Prog. Lang. Syst.\u00a016(6) (1994)","DOI":"10.1145\/197320.197383"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45651-1","volume-title":"Modular Specification and Verification of Object-Oriented Programs","author":"P. M\u00fcller","year":"2002","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262. Springer, Heidelberg (2002)"},{"key":"13_CR31","unstructured":"M\u00fcller, P.: Reasoning about object structures using ownership. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)"},{"issue":"1","key":"13_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0167-6423(00)00005-8","volume":"41","author":"D.A. Naumann","year":"2001","unstructured":"Naumann, D.A.: Predicate transformer semantics of a higher order imperative language with record subtyping. Sci. Comput. Programming\u00a041(1), 1\u201351 (2001)","journal-title":"Sci. Comput. Programming"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/11561163_11","volume-title":"Formal Methods for Components and Objects","author":"D.A. Naumann","year":"2005","unstructured":"Naumann, D.A.: Assertion-Based Encapsulation, Object Invariants and Simulations. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol.\u00a03657, pp. 251\u2013273. Springer, Heidelberg (2005)"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11541868_14","volume-title":"Theorem Proving in Higher Order Logics","author":"D.A. Naumann","year":"2005","unstructured":"Naumann, D.A.: Verifying a Secure Information Flow Analyzer. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 211\u2013226. Springer, Heidelberg (2005)"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11863908_18","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D.A. Naumann","year":"2006","unstructured":"Naumann, D.A.: From Coupling Relations to Mated Invariants for Checking Information Flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 279\u2013296. Springer, Heidelberg (2006)"},{"key":"13_CR36","unstructured":"Naumann, D.A.: Observational purity and encapsulation. Theoretical Comput. Sci. (to appear, 2006)"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state (extended abstract). In: IEEE Symp. on Logic in Computer Science (LICS), pp. 313\u2013323 (2004)","DOI":"10.1109\/LICS.2004.1319626"},{"key":"13_CR38","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.tcs.2006.07.035","volume":"365","author":"D.A. Naumann","year":"2006","unstructured":"Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoretical Comput. Sci.\u00a0365, 143\u2013168 (2006); Extended version of [37]","journal-title":"Theoretical Comput. Sci."},{"key":"13_CR39","unstructured":"O\u2019Hearn, P.: Scalable specification and reasoning: Technical challenges for program logic. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: ACM Symp. on Princ. of Program. Lang. (POPL), pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"key":"13_CR41","unstructured":"Parkinson, M.J.: Local reasoning for Java. Technical Report 654, University of Cambridge Computer Laboratory, Dissertation (November 2005)"},{"key":"13_CR42","first-page":"717","volume-title":"Proceedings of the ACM Annual Conference","author":"J.C. Reynolds","year":"1972","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference, vol.\u00a02, pp. 717\u2013740. ACM Press, New York (1972)"},{"key":"13_CR43","volume-title":"The Craft of Programming","author":"J.C. Reynolds","year":"1981","unstructured":"Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"13_CR44","volume-title":"Algorithmic Languages","author":"J.C. Reynolds","year":"1981","unstructured":"Reynolds, J.C.: The essence of Algol. In: de Bakker, J.W., van Vliet, J.C. (eds.) Algorithmic Languages, North-Holland, Amsterdam (1981)"},{"key":"13_CR45","unstructured":"Reynolds, J.C.: An overview of separation logic. In: Meyer, B., Woodcock, J.C.P. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE) (2005)"},{"key":"13_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/11531142_24","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"E. Rodr\u00edguez","year":"2005","unstructured":"Rodr\u00edguez, E., Dwyer, M., Flanagan, C., Hatcliff, J., Leavens, G.T., Robby, F.: Extending JML for Modular Specification and Verification of Multi-threaded Programs. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 551\u2013576. Springer, Heidelberg (2005)"},{"issue":"1","key":"13_CR47","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE J. Selected Areas in Communications"},{"key":"13_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-27864-1_9","volume-title":"Static Analysis","author":"Q. Sun","year":"2004","unstructured":"Sun, Q., Banerjee, A., Naumann, D.A.: Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 84\u201399. Springer, Heidelberg (2004)"},{"key":"13_CR49","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.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"key":"13_CR50","unstructured":"Yang, H.: Relational separation logic. Theoretical Comput. Sci. (to appear, 2004)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:42:51Z","timestamp":1557718971000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}