{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:19:58Z","timestamp":1740028798497,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433538"},{"type":"electronic","value":"9783540459231"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45923-5_2","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"15-32","source":"Crossref","is-referenced-by-count":7,"title":["Compositional Verification of Secure Applet Interactions"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,15]]},"reference":[{"unstructured":"G. Barthe, D. Gurov, and M. Huisman. Compositional specification and verification of control flow based security properties of multi-application programs. In Proceedings of Workshop on Formal Techniques for Java Programs (FTfJP), 2001.","key":"2_CR1"},{"doi-asserted-by":"crossref","unstructured":"P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, and J.-L. Lanet. Electronic purse applet certification: extended abstract. In S. Schneider and P. Ryan, editors, Proceedings of the workshop on secure architectures and information flow, volume 32 of Elect. Notes in Theor. Comp. Sci. Elsevier Publishing, 2000.","key":"2_CR2","DOI":"10.1016\/S1571-0661(04)00092-1"},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Model checking the full modal mu-calculus for infinite sequential processes","author":"O. Burkart","year":"1997","unstructured":"O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. In Proceedings of ICALP\u201997, number 1256 in LNCS, pages 419\u2013429, 1997."},{"issue":"4","key":"2_CR4","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model checker. Software Tools for Technology Transfer (STTT), 2\/4:410\u2013425, 2000.","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_13","volume-title":"SPIN Model Checking and Software Verification","author":"J. Corbett","year":"2000","unstructured":"J. Corbett, M. Dwyer, J. Hatcli., and Robby. A language framework for expressing checkable properties of dynamic software. In K. Havelund, J. Penix, and W. Visser, editors, SPIN Model Checking and Software Verification, number 1885 in LNCS. Springer, 2000."},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","first-page":"247","volume-title":"Compositional verification of CCS processes","author":"M. Dam","year":"1999","unstructured":"M. Dam and D. Gurov. Compositional verification of CCS processes. In D. Bj\u00f8rner, M. Broy, and A.V. Zamulin, editors, Proceedings of PSI\u201999, number 1755 in LNCS, pages 247\u2013256, 1999."},{"unstructured":"M. Dam and D. Gurov. \u03bc-calculus with explicit points and approximations. Journal of Logic and Computation, 2001. To appear.","key":"2_CR7"},{"doi-asserted-by":"crossref","unstructured":"L.-\u00e5. Fredlund, D. Gurov, T. Noll, M. Dam, T. Arts, and G. Chugunov. A verification tool for Erlang. Software Tools for Technology Transfer (STTT), 2002. To appear.","key":"2_CR8","DOI":"10.1007\/s100090100071"},{"issue":"5","key":"2_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The model checker SPIN. Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"T. Jensen, D. Le M\u00e9tayer, and T. Thorn. Verification of control flow based security policies. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 89\u2013103. IEEE Computer Society Press, 1999.","key":"2_CR10","DOI":"10.1109\/SECPRI.1999.766902"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"2_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Java bytecode verification: an overview","author":"X. Leroy","year":"2001","unstructured":"X. Leroy. Java bytecode verification: an overview. In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV\u201901, number 2102 in LNCS, pages 265\u2013285. Springer, 2001."},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-45418-7_13","volume-title":"Smart Card Programming and Security (E-Smart 2001)","author":"X. Leroy","year":"2001","unstructured":"X. Leroy. On-card bytecode verification for JavaCard. In I. Attali and T. Jensen, editors, Smart Card Programming and Security (E-Smart 2001), number 2140 in LNCS, pages 150\u2013164. Springer, 2001."},{"issue":"2","key":"2_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"A. Simpson. Compositionality via cut-elimination: Hennesy-Milner logic for an arbitrary GSOS. In Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 420\u2013430, 1995.","key":"2_CR15","DOI":"10.1109\/LICS.1995.523276"},{"doi-asserted-by":"crossref","unstructured":"G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In Proceedings of POPL\u201998, pages 355\u2013364. ACM Press, 1998.","key":"2_CR16","DOI":"10.1145\/268946.268975"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45923-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:12:52Z","timestamp":1739992372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45923-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433538","9783540459231"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45923-5_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}