{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:24:23Z","timestamp":1763724263462},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642197505"},{"type":"electronic","value":"9783642197512"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-19751-2_5","type":"book-chapter","created":{"date-parts":[[2011,2,24]],"date-time":"2011-02-24T05:55:17Z","timestamp":1298526917000},"page":"65-79","source":"Crossref","is-referenced-by-count":4,"title":["Information Flow Analysis via Path Condition Refinement"],"prefix":"10.1007","author":[{"given":"Mana","family":"Taghdiri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregor","family":"Snelting","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software, pp. 103\u2013122 (2001)","DOI":"10.1007\/3-540-45139-0_7"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-540-75336-0_2","volume-title":"Trustworthy Global Computing","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Beringer, L., Cr\u00e9gut, P., Gr\u00e9goire, B., Hofmann, M.O., M\u00fcller, P., Poll, E., Puebla, G., Stark, I., V\u00e9tillard, E.: Mobius: Mobility, ubiquity, security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 10\u201329. Springer, Heidelberg (2007)"},{"issue":"6","key":"5_CR3","doi-asserted-by":"publisher","first-page":"647","DOI":"10.3233\/JCS-2007-15604","volume":"15","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Nieto, L.P.: Secure information flow for a concurrent language with scheduling. Journal of Computer Security\u00a015(6), 647\u2013689 (2007)","journal-title":"Journal of Computer Security"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M. Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 294\u2013298. Springer, Heidelberg (2008)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathSAT\u00a04 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B., et al.: Efficiently computing static single assignment and control dependence graph. TOPLAS\u00a013(4), 451\u2013490 (1991)","journal-title":"TOPLAS"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"2","key":"5_CR9","first-page":"197","volume":"16","author":"D. Giffhorn","year":"2009","unstructured":"Giffhorn, D., Hammer, C.: Precise slicing of concurrent programs, an evaluation of precise slicing algorithms for concurrent programs. JASE\u00a016(2), 197\u2013234 (2009)","journal-title":"JASE"},{"key":"5_CR10","unstructured":"Hammer, C.: Information Flow Control for Java, A Comprehensive Approach on Path Conditions in Dependence Graphs. PhD thesis, Universit\u00e4t Karlsruhe (2009)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-11747-3_4","volume-title":"Engineering Secure Software and Systems","author":"C. Hammer","year":"2010","unstructured":"Hammer, C.: Experiences with PDG-based IFC. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol.\u00a05965, pp. 44\u201360. Springer, Heidelberg (2010)"},{"issue":"6","key":"5_CR12","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C. Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. J. of Information Security\u00a08(6), 399\u2013422 (2009)","journal-title":"J. of Information Security"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"5_CR14","first-page":"79","volume-title":"POPL 2006","author":"S. Hunt","year":"2006","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79\u201390. ACM, New York (2006)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-01702-5_1","volume-title":"Hardware and Software: Verification and Testing","author":"D. Jackson","year":"2009","unstructured":"Jackson, D.: Hazards of verification. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, p. 1. Springer, Heidelberg (2009)"},{"key":"5_CR16","first-page":"178","volume-title":"ESEC\/FSE 2003","author":"J. Krinke","year":"2003","unstructured":"Krinke, J.: Context-sensitive slicing of concurrent programs. In: ESEC\/FSE 2003, pp. 178\u2013187. ACM, New York (2003)"},{"key":"5_CR17","series-title":"Recent Advances","volume-title":"Handbook of Software Engineering and Knowledge Engineering","author":"J. Krinke","year":"2005","unstructured":"Krinke, J.: Program slicing. In: Handbook of Software Engineering and Knowledge Engineering. Recent Advances, vol.\u00a03. World Scientific Publishing, Singapore (2005)"},{"key":"5_CR18","first-page":"228","volume-title":"POPL 1999","author":"A.C. Myers","year":"1999","unstructured":"Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL 1999, pp. 228\u2013241. ACM Press, New York (1999)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: Armc: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021(1) (January 2003)","DOI":"10.1109\/JSAC.2002.806121"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-03237-0_3","volume-title":"Static Analysis","author":"M. Seghir","year":"2009","unstructured":"Seghir, M., Podelski, A., Wies, T.: Abstraction refinement for quantified array assertions. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 3\u201318. Springer, Heidelberg (2009)"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: POPL 1998, San Diego, CA, pp. 355\u2013364 (January 1998)","DOI":"10.1145\/268946.268975"},{"issue":"4","key":"5_CR23","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/1178625.1178628","volume":"15","author":"G. Snelting","year":"2006","unstructured":"Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. TOSEM\u00a015(4), 410\u2013457 (2006)","journal-title":"TOSEM"},{"issue":"1","key":"5_CR24","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10515-006-0005-x","volume":"14","author":"M. Taghdiri","year":"2007","unstructured":"Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Journal of Automated Software Engineering\u00a014(1), 87\u2013121 (2007)","journal-title":"Journal of Automated Software Engineering"},{"key":"5_CR25","first-page":"87","volume-title":"PLDI 2009","author":"O. Tripp","year":"2009","unstructured":"Tripp, O., Pistoia, M., Fink, S., Sridharan, M., Weismani, O.: TAJ: effective taint analysis of web applications. In: PLDI 2009, pp. 87\u201397. ACM, New York (2009)"},{"key":"5_CR26","unstructured":"Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: VERIFY 2010 (2010)"},{"key":"5_CR27","volume-title":"PLAS 2009","author":"D. Wasserrab","year":"2009","unstructured":"Wasserrab, D., Lohner, D., Snelting, G.: On PDG-based noninterference and its modular proof. In: PLAS 2009. ACM, New York (2009)"},{"key":"5_CR28","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker. In: DATE 2003, pp. 10880\u201310886 (2003)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19751-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T04:34:43Z","timestamp":1558413283000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19751-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642197505","9783642197512"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19751-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}