{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T22:10:05Z","timestamp":1748815805725,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496343"},{"type":"electronic","value":"9783662496350"}],"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-662-49635-0_6","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T12:03:52Z","timestamp":1458561832000},"page":"97-115","source":"Crossref","is-referenced-by-count":1,"title":["Towards Fully Automatic Logic-Based Information Flow Analysis: An\u00a0Electronic-Voting Case Study"],"prefix":"10.1007","author":[{"given":"Quoc Huy","family":"Do","sequence":"first","affiliation":[]},{"given":"Eduard","family":"Kamburjan","sequence":"additional","affiliation":[]},{"given":"Nathan","family":"Wasser","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"11","key":"6_CR1","doi-asserted-by":"publisher","first-page":"2479","DOI":"10.1016\/j.jss.2012.05.061","volume":"85","author":"M Avvenuti","year":"2012","unstructured":"Avvenuti, M., Bernardeschi, C., Francesco, N.D., Masci, P.: JCSI: a tool for checking secure information flow in java card applications. J. Syst. Softw. 85(11), 2479\u20132493 (2012)","journal-title":"J. Syst. Softw."},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.entcs.2007.02.027","volume":"173","author":"A Banerjee","year":"2007","unstructured":"Banerjee, A., Giacobazzi, R., Mastroeni, I.: What you lose is what you leak: information leakage in declassification policies. Electron. Notes Theor. Comput. Sci. 173, 47\u201366 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"6_CR3","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 Workshop on Computer Security Foundations, CSFW 2004, pp. 100\u2013114. IEEE CS(2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-319-14125-1_2","volume-title":"Logic-Based Program Synthesis and Transformation","author":"B Beckert","year":"2014","unstructured":"Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Information flow in object-oriented software. In: Gupta, G., Pe\u00f1a, R. (eds.) LOPSTR 2013, LNCS 8901. LNCS, vol. 8901, pp. 19\u201337. Springer, Heidelberg (2014)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. Lecture Notes in Computer Science, vol. 4334. Springer, Heidelberg (2007)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-04167-9_13","volume-title":"Formal Methods for Components and Objects","author":"R Bubel","year":"2009","unstructured":"Bubel, R., H\u00e4hnle, R., Wei\u00df, B.: Abstract interpretation of symbolic execution with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 247\u2013277. Springer, Heidelberg (2009)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Symposium on Principles of Programming Languages (POPL), pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/1925844.1926399","volume":"46","author":"P Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. SIGPLAN Not. 46(1), 105\u2013118 (2011)","journal-title":"SIGPLAN Not."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"6_CR10","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Gorrieri, R. (ed.) Workshop on Issues in the Theory of Security. IFIP WG 1.7, SIGPLAN and GI FoMSESS. ACM (2003)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"6_CR12","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-319-18467-8_27","volume-title":"ICT SystemsSecurity and Privacy Protection","author":"Q Do","year":"2015","unstructured":"Do, Q., Bubel, R., H\u00e4hnle, R.: Exploit generation for information flow leaks in object oriented programs. In: Federrath, H., Gollmann, D. (eds.) ICT SystemsSecurity and Privacy Protection. IFIP Advances in Information and Communication Technology, vol. 455, pp. 401\u2013415. Springer, Heidelberg (2015)"},{"issue":"1","key":"6_CR13","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/565816.503291","volume":"37","author":"C Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. SIGPLAN Not. 37(1), 191\u2013202 (2002)","journal-title":"SIGPLAN Not."},{"key":"6_CR14","unstructured":"Graf, J., Hecker, M., Mohr, M.: Using JOANA for information flow control in java programs - a practical guide. In: Proceedings of the 6th Working Conference on Programming Languages. LNI, vol. 215, pp. 123\u2013138. Springer, February 2013"},{"issue":"6","key":"6_CR15","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/1379022.1375623","volume":"43","author":"N Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. SIGPLAN Not. 43(6), 339\u2013348 (2008)","journal-title":"SIGPLAN Not."},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/978-3-319-09099-3_7","volume-title":"Tests and Proofs","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: Visualizing unbounded symbolic execution. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 82\u201398. Springer, Heidelberg (2014)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: ACM SIGPLAN Notices, vol. 41, pp. 79\u201390. ACM (2006)","DOI":"10.1145\/1111320.1111045"},{"key":"6_CR18","unstructured":"Janota, M.: Assertion-based loop invariant generation. In: Proceedings of the 1st International Workshop on Invariant Generation (WING 07), Wing 2004 (2007)"},{"issue":"7","key":"6_CR19","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"6_CR20","unstructured":"K\u00fcsters, R., Truderung, T., Beckert, B., Bruns, D., Graf, J., Scheben, C.: A hybrid approach for proving noninterference and applications to the cryptographic verification of java programs. In: Grande Region Security and Reliability Day 2013, Extended Abstract (2013)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Beckert, B., Bruns, D., Kirsten, M., Mohr, M.: A hybrid approach for proving noninterference of java programs. In: Fournet, C., Hicks, M. (eds.) 28th IEEE Computer Security Foundations Symposium (2015)","DOI":"10.1109\/CSF.2015.28"},{"key":"6_CR22","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a java modeling language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998), pp. 404\u2013420 (1998)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Proceedings of the 2009 ACM Symposium on Applied Computing, SAC 2009, pp. 615\u2013622. ACM, New York (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: Proceedings of 26th ACM Symposium on Principles of Programming Languages, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-37621-7_9","volume-title":"Software Security - Theories and Systems","author":"A Sabelfeld","year":"2004","unstructured":"Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) Software Security - Theories and Systems. Lecture Notes in Computer Science, vol. 3233, pp. 174\u2013191. Springer, Heidelberg (2004)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-31762-0_15","volume-title":"Formal Verification of Object-Oriented Software","author":"C Scheben","year":"2012","unstructured":"Scheben, C., Schmitt, P.H.: Verification of information flow properties of java programs without approximations. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 232\u2013249. Springer, Heidelberg (2012)"},{"issue":"2","key":"6_CR27","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2), 167\u2013187 (1996)","journal-title":"J. Comput. Secur."},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-25942-0_16","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"N Wasser","year":"2015","unstructured":"Wasser, N.: Generating specifications for recursive methods by abstracting program states. In: Li, X., Liu, Z., Yi, W. (eds.) Dependable Software Engineering: Theories, Tools, and Applications. Lecture Notes in Computer Science, vol. 9409, pp. 243\u2013257. Springer, Heidelberg (2015)"},{"key":"6_CR29","unstructured":"Wasser, N., Bubel, R.: A theorem prover backed approach to array abstraction. Technical. report, Department of Computer Science, Technische Universit\u00e4t Darmstadt, Germany , presented at the Vienna Summer of Logic 2014 5th International Workshop on Invariant Generation (2014)"},{"key":"6_CR30","unstructured":"Wasser, N., Bubel, R., H\u00e4hnle, R.: Array abstraction with symbolic pivots. Technical report, Department of Computer Science, Technische Universit\u00e4t Darmstadt, Germany, August 2015"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49635-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:32:58Z","timestamp":1748813578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49635-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496343","9783662496350"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49635-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}