{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:50:10Z","timestamp":1768283410966,"version":"3.49.0"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031505201","type":"print"},{"value":"9783031505218","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-50521-8_15","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T08:03:15Z","timestamp":1703836995000},"page":"314-337","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Sound Abstract Nonexploitability Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1077-7812","authenticated-orcid":false,"given":"Francesco","family":"Parolini","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-3179","authenticated-orcid":false,"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"15_CR1","unstructured":"Common vulnerabilities and exposures (CVE) database. https:\/\/cve.mitre.org\/. Accessed 30 Aug 2023"},{"key":"15_CR2","unstructured":"CVE-2019-8745. Available from NIST, CVE-ID CVE-2019-8745. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2019-8745. Accessed 30 Aug 2023"},{"key":"15_CR3","unstructured":"CVE-2022-36934. Available from NIST, CVE-ID CVE-2022-36934. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2022-36934. Accessed 30 Aug 2023"},{"key":"15_CR4","unstructured":"CVE-2022-4135. Available from NIST, CVE-ID CVE-2022-4135. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2022-4135 Accessed 30 Aug 2023"},{"key":"15_CR5","unstructured":"The Infer static analyzer. https:\/\/fbinfer.com\/"},{"key":"15_CR6","unstructured":"The Pysa static analyzer. https:\/\/engineering.fb.com\/2020\/08\/07\/security\/pysa\/"},{"key":"15_CR7","unstructured":"Juliet C\/C++ test suite (2017). https:\/\/samate.nist.gov\/SARD\/test-suites\/112. Accessed 30 Aug 2023"},{"key":"15_CR8","unstructured":"Microsoft: a proactive approach to more secure code (2019). https:\/\/msrc.microsoft.com\/blog\/2019\/07\/a-proactive-approach-to-more-secure-code\/. Accessed 30 Aug 2023"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Agat, J.: Transforming out timing leaks. In: Principles of Programming Languages, POPL, pp. 40\u201353. ACM (2000). https:\/\/doi.org\/10.1145\/325694.325702","DOI":"10.1145\/325694.325702"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: Conference on Programming Language Design and Implementation, PLDI, pp. 362\u2013375. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062378","DOI":"10.1145\/3062341.3062378"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Arzt, S., et al.: FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps. In: Programming Language Design and Implementation, PLDI, pp. 259\u2013269. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594299","DOI":"10.1145\/2594291.2594299"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting semantics and its application to static analysis of information flow. In: Principles of Programming Languages, POPL (2017). https:\/\/doi.org\/10.1145\/3009837.3009889","DOI":"10.1145\/3009837.3009889"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269\u2013276. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_75"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: Computer Security Foundations Workshop CSFW, pp. 253. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/CSFW.2002.1021820","DOI":"10.1109\/CSFW.2002.1021820"},{"key":"15_CR15","unstructured":"Bardin, S., Girol, G.: A quantitative flavour of robust reachability. CoRR abs\/2212.05244 (2022). 10.48550\/arXiv. 2212.05244"},{"issue":"6","key":"15_CR16","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). https:\/\/doi.org\/10.1017\/S0960129511000193","journal-title":"Math. Struct. Comput. Sci."},{"issue":"12","key":"15_CR17","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/501317.501328","volume":"44","author":"H Berghel","year":"2001","unstructured":"Berghel, H.: The code red worm. Commun. ACM 44(12), 15\u201319 (2001). https:\/\/doi.org\/10.1145\/501317.501328","journal-title":"Commun. ACM"},{"key":"15_CR18","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). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: 21st IEEE Computer Security Foundations Symposium, pp. 51\u201365 (2008)","DOI":"10.1109\/CSF.2008.7"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Cohen, E.S.: Information transmission in computational systems. In: Symposium on Operating System Principles, SOSP, pp. 133\u2013139. ACM (1977). https:\/\/doi.org\/10.1145\/800214.806556","DOI":"10.1145\/800214.806556"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-32304-2_19","volume-title":"Static Analysis","author":"P Cousot","year":"2019","unstructured":"Cousot, P.: Abstract semantic dependency. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 389\u2013410. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_19"},{"key":"15_CR23","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973","volume-title":"Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints","author":"P Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Principles of Programming Languages, POPL (1977)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28869-2_9","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2012","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_9"},{"issue":"7","key":"15_CR25","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977). https:\/\/doi.org\/10.1145\/359636.359712","journal-title":"Commun. ACM"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Durumeric, Z., et al.: The matter of heartbleed. In: Internet Measurement Conference, IMC, pp. 475\u2013488. ACM (2014). https:\/\/doi.org\/10.1145\/2663716.2663755","DOI":"10.1145\/2663716.2663755"},{"key":"15_CR27","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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1007\/978-3-030-81685-8_32","volume-title":"Computer Aided Verification","author":"G Girol","year":"2021","unstructured":"Girol, G., Farinier, B., Bardin, S.: Not all bugs are created equal, but robust reachability can tell the difference. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 669\u2013693. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_32"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Security and Privacy, pp. 11\u201320. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Security and Privacy, pp. 75\u201387. IEEE Computer Society (1984). https:\/\/doi.org\/10.1109\/SP.1984.10019","DOI":"10.1109\/SP.1984.10019"},{"issue":"5","key":"15_CR31","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994). https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Aspects Comput."},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Heintze, N., Riecke, J.G.: The slam calculus: programming with secrecy and integrity. In: Principles of Programming Languages, POPL, pp. 365\u2013377. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268976","DOI":"10.1145\/268946.268976"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: Annual Computer Security Applications Conference, ACSAC, pp. 261\u2013269. ACM (2010). https:\/\/doi.org\/10.1145\/1920261.1920300","DOI":"10.1145\/1920261.1920300"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"15_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-41600-3_1","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"M Journault","year":"2020","unstructured":"Journault, M., Min\u00e9, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 1\u201318. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_1"},{"key":"15_CR36","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.infsof.2017.04.001","volume":"88","author":"L Li","year":"2017","unstructured":"Li, L., et al.: Static analysis of android apps: a systematic literature review. Inf. Softw. Technol. 88, 67\u201395 (2017). https:\/\/doi.org\/10.1016\/j.infsof.2017.04.001","journal-title":"Inf. Softw. Technol."},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Mastroeni, I., Pasqua, M.: Hyperhierarchy of semantics - a formal framework for hyperproperties verification. In: Static Analysis Symposium, SAS. vol. 10422, pp. 232\u2013252 (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_12","DOI":"10.1007\/978-3-319-66706-5_12"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Mastroeni, I., Pasqua, M.: Verifying bounded subset-closed hyperproperties. In: Static Analysis Symposium, SAS. vol. 11002, pp. 263\u2013283 (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_17","DOI":"10.1007\/978-3-319-99725-4_17"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"Mastroeni, I., Pasqua, M.: Statically analyzing information flows: an abstract interpretation-based hyperanalysis for non-interference. In: Symposium on Applied Computing, SAC, pp. 2215\u20132223 (2019). https:\/\/doi.org\/10.1145\/3297280.3297498","DOI":"10.1145\/3297280.3297498"},{"key":"15_CR40","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symbolic Comput. (HOSC) 19(1), 31\u2013100 (2006). https:\/\/doi.org\/10.1007\/s10990-006-8609-1, http:\/\/www-apr.lip6.fr\/mine\/publi\/article-mine-HOSC06.pdf","DOI":"10.1007\/s10990-006-8609-1"},{"key":"15_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322\u2013339. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-45099-3_17"},{"key":"15_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-47764-0_7","volume-title":"Static Analysis","author":"D Monniaux","year":"2001","unstructured":"Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 111\u2013126. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0_7"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Symposium on Operating System Principles, SOSP, pp. 129\u2013142. ACM (1997). https:\/\/doi.org\/10.1145\/268998.266669","DOI":"10.1145\/268998.266669"},{"issue":"6","key":"15_CR44","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1017\/s0956796897002906","volume":"7","author":"P \u00d8rb\u00e6k","year":"1997","unstructured":"\u00d8rb\u00e6k, P., Palsberg, J.: Trust in the lambda-calculus. J. Funct. Program. 7(6), 557\u2013591 (1997). https:\/\/doi.org\/10.1017\/s0956796897002906","journal-title":"J. Funct. Program."},{"issue":"5","key":"15_CR45","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1109\/MSECP.2003.1236233","volume":"1","author":"HK Orman","year":"2003","unstructured":"Orman, H.K.: The Morris worm: a fifteen-year perspective. IEEE Secur. Priv. 1(5), 35\u201343 (2003). https:\/\/doi.org\/10.1109\/MSECP.2003.1236233","journal-title":"IEEE Secur. Priv."},{"key":"15_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-65474-0_11","volume-title":"Static Analysis","author":"A Ouadjaout","year":"2020","unstructured":"Ouadjaout, A., Min\u00e9, A.: A library modeling language for the static analysis of C programs. In: Pichardie, D., Sighireanu, M. (eds.) SAS 2020. LNCS, vol. 12389, pp. 223\u2013247. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-65474-0_11"},{"key":"15_CR47","doi-asserted-by":"publisher","unstructured":"Parolini, F., Min\u00e9, A.: Sound Abstract Nonexploitability Analysis Artifact (2023). https:\/\/doi.org\/10.5281\/zenodo.8334112","DOI":"10.5281\/zenodo.8334112"},{"key":"15_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-319-27810-0_6","volume-title":"Semantics, Logics, and Calculi","author":"A Di Pierro","year":"2016","unstructured":"Di Pierro, A., Wiklicky, H.: Probabilistic abstract interpretation: from trace semantics to DTMC\u2019s and linear regression. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi. LNCS, vol. 9560, pp. 111\u2013139. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-27810-0_6"},{"issue":"1","key":"15_CR49","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. ACM Trans. Program. Lang. Syst. 25(1), 117\u2013158 (2003). https:\/\/doi.org\/10.1145\/596980.596983","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR50","doi-asserted-by":"publisher","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Computer Security Foundations Workshop, CSFW, pp. 200\u2013214. IEEE Computer Society (2000). https:\/\/doi.org\/10.1109\/CSFW.2000.856937","DOI":"10.1109\/CSFW.2000.856937"},{"issue":"3","key":"15_CR51","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1016\/S1353-4858(03)00310-6","volume":"2003","author":"E Schultz","year":"2003","unstructured":"Schultz, E., Mellander, J., Peterson, D.: The MS-SQL slammer worm. Netw. Secur. 2003(3), 10\u201314 (2003). https:\/\/doi.org\/10.1016\/S1353-4858(03)00310-6","journal-title":"Netw. Secur."},{"key":"15_CR52","doi-asserted-by":"publisher","unstructured":"Smith, G., Volpano, D.M.: Secure information flow in a multi-threaded imperative language. In: Principles of Programming Languages, POPL, pp. 355\u2013364. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268975","DOI":"10.1145\/268946.268975"},{"key":"15_CR53","doi-asserted-by":"publisher","unstructured":"Spoto, F., et al.: Static identification of injection attacks in Java. ACM Trans. Program. Lang. Syst. 41(3), 18:1\u201318:58 (2019). https:\/\/doi.org\/10.1145\/3332371","DOI":"10.1145\/3332371"},{"key":"15_CR54","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). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"15_CR55","doi-asserted-by":"publisher","unstructured":"Tiraboschi, I., Rezk, T., Rival, X.: Sound symbolic execution via abstract interpretation and its application to security. In: Verification, Model Checking, and Abstract Interpretation, VMCAI. LNCS, vol. 13881, pp. 267\u2013295. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_13","DOI":"10.1007\/978-3-031-24950-1_13"},{"key":"15_CR56","doi-asserted-by":"publisher","unstructured":"Urban, C., M\u00fcller, P.: An abstract interpretation framework for input data usage. In: European Symposium on Programming, ESOP. vol. 10801, pp. 683\u2013710 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_24","DOI":"10.1007\/978-3-319-89884-1_24"},{"issue":"2\/3","key":"15_CR57","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"DM Volpano","year":"1996","unstructured":"Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\/3), 167\u2013188 (1996). https:\/\/doi.org\/10.3233\/JCS-1996-42-304","journal-title":"J. Comput. Secur."},{"key":"15_CR58","doi-asserted-by":"publisher","unstructured":"Volpano, D.M., Smith, G.: Probabilistic noninterference in a concurrent language. J. Comput. Secur. 7(1), 231\u2013253 (1999). https:\/\/doi.org\/10.3233\/jcs-1999-72-305","DOI":"10.3233\/jcs-1999-72-305"},{"key":"15_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-45309-1_4","volume-title":"Programming Languages and Systems","author":"S Zdancewic","year":"2001","unstructured":"Zdancewic, S., Myers, A.C.: Secure information flow and CPS. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 46\u201361. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45309-1_4"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-50521-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:10:09Z","timestamp":1704240609000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50521-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505201","9783031505218"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50521-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}