{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:04Z","timestamp":1760202664415,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642365621"},{"type":"electronic","value":"9783642365638"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36563-8_8","type":"book-chapter","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T06:32:47Z","timestamp":1361514767000},"page":"107-122","source":"Crossref","is-referenced-by-count":8,"title":["Confidentiality for Probabilistic Multi-threaded Programs and Its Verification"],"prefix":"10.1007","author":[{"given":"Tri","family":"Minh Ngo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Aho, A.V., Hopcroft, J.E.: The Design and Analysis of Computer Algorithms, 1st edn. Addison-Wesley (1974)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-22012-8_4","volume-title":"Automata, Languages and Programming","author":"M.S. Alvim","year":"2011","unstructured":"Alvim, M.S., Andr\u00e9s, M.E., Chatzikokolakis, K., Palamidessi, C.: On the Relation between Differential Privacy and Quantitative Information Flow. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol.\u00a06756, pp. 60\u201376. Springer, Heidelberg (2011)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-23082-0_8","volume-title":"Foundations of Security Analysis and Design VI","author":"M.S. Alvim","year":"2011","unstructured":"Alvim, M.S., Andr\u00e9s, M.E., Chatzikokolakis, K., Palamidessi, C.: Quantitative Information Flow and Applications to Differential Privacy. In: Aldini, A., Gorrieri, R. (eds.) FOSAD VI 2011. LNCS, vol.\u00a06858, pp. 211\u2013230. Springer, Heidelberg (2011)"},{"issue":"28","key":"8_CR4","doi-asserted-by":"publisher","first-page":"3072","DOI":"10.1016\/j.tcs.2011.02.045","volume":"412","author":"M.E. Andres","year":"2011","unstructured":"Andres, M.E., Palamidessi, C., Sokolova, A., Van Rossum, P.: Information hiding in probabilistic concurrent systems. Journal of Theoretical Computer Science\u00a0412(28), 3072\u20133089 (2011)","journal-title":"Journal of Theoretical Computer Science"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0020-0190(98)00038-6","volume":"66","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters\u00a066, 71\u201379 (1998)","journal-title":"Information Processing Letters"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100\u2013114. IEEE Press (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and Symbolic Reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 354\u2013359. Springer, Heidelberg (2010)"},{"key":"8_CR8","unstructured":"Blondeel, H.-C.: Security by logic: characterizing non-interference in temporal logic. Master\u2019s thesis, KTH Sweden (2007)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chen, H., Malacaria, P.: Quantitative analysis of leakage for multi-threaded programs. In: PLAS 2007 (2007)","DOI":"10.1145\/1255329.1255335"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/3-540-55179-4_30","volume-title":"Computer Aided Verification","author":"L. Christoff","year":"1992","unstructured":"Christoff, L., Christoff, I.: Efficient Algorithms for Verification of Equivalences for Probabilistic Processes. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 310\u2013321. Springer, Heidelberg (1992)"},{"issue":"3","key":"8_CR11","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1142\/S0129054108005814","volume":"19","author":"L.. Doyen","year":"2008","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci.\u00a019(3), 549\u2013563 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11691372_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why Waste a Perfectly Good Abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 212\u2013226. Springer, Heidelberg (2006)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-31762-0_12","volume-title":"Formal Verification of Object-Oriented Software","author":"M. Huisman","year":"2012","unstructured":"Huisman, M., Ngo, T.M.: Scheduler-Specific Confidentiality for Multi-threaded Programs and Its Logic-Based Verification. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 178\u2013195. Springer, Heidelberg (2012)"},{"key":"8_CR15","unstructured":"Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterization of observation determinism. In: CSFW. IEEE Computer Society (2006)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-642-22110-1_42","volume-title":"Computer Aided Verification","author":"S. Kiefer","year":"2011","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Language\u00a0Equivalence\u00a0for Probabilistic\u00a0Automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 526\u2013540. Springer, Heidelberg (2011)"},{"key":"8_CR17","first-page":"83","volume":"16","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical considerations on modal logic. Acta Philosophica Fennica\u00a016, 83\u201394 (1963)","journal-title":"Acta Philosophica Fennica"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218\u2013232 (2011)","DOI":"10.1109\/CSF.2011.22"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-15497-3_8","volume-title":"Computer Security \u2013 ESORICS 2010","author":"H. Mantel","year":"2010","unstructured":"Mantel, H., Sudbrock, H.: Flexible Scheduler-Independent Security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol.\u00a06345, pp. 116\u2013133. Springer, Heidelberg (2010)"},{"key":"8_CR20","unstructured":"Ngo, T.M., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. Full version, http:\/\/wwwhome.ewi.utwente.nl\/~ngominhtri\/"},{"key":"8_CR21","unstructured":"Ngo, T.M., Stoelinga, M., Huisman, M.: Effective verification of confidentiality for multi-threaded programs. Manuscript 201X"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0020-0190(97)00133-6","volume":"63","author":"D. Peled","year":"1997","unstructured":"Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters\u00a063, 243\u2013246 (1997)","journal-title":"Information Processing Letters"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: CSP and determinism in security modeling. In: IEEE Symposium on Security and Privacy, pp. 114\u2013127. IEEE Computer Society (1995)","DOI":"10.1109\/SECPRI.1995.398927"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW, pp. 200\u2013214 (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: CSFW (2003)","DOI":"10.1109\/CSFW.2003.1212701"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G. Smith","year":"2009","unstructured":"Smith, G.: On the Foundations of Quantitative Information Flow. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 288\u2013302. Springer, Heidelberg (2009)"},{"key":"8_CR27","unstructured":"Stoelinga, M.I.A.: Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, The Netherlands (April 2002)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: A type system for observational determinism. In: CSF (2008)","DOI":"10.1109\/CSF.2008.9"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1137\/0221017","volume":"21","author":"W.G. Tzeng","year":"1992","unstructured":"Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing\u00a021, 216\u2013227 (1992)","journal-title":"SIAM Journal on Computing"},{"key":"8_CR30","doi-asserted-by":"crossref","first-page":"231","DOI":"10.3233\/JCS-1999-72-305","volume":"7","author":"D. Volpano","year":"1999","unstructured":"Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security\u00a07, 231\u2013253 (1999)","journal-title":"Journal of Computer Security"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW, pp. 29\u201343. IEEE (2003)","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Zhu, J., Srivatsa, M.: Quantifying information leakage in finite order deterministic programs. In: CoRR 2010 (2010)","DOI":"10.1109\/icc.2011.5963509"}],"container-title":["Lecture Notes in Computer Science","Engineering Secure Software and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36563-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:58:01Z","timestamp":1745963881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36563-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642365621","9783642365638"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36563-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}