{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:10:49Z","timestamp":1763467849820,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68237-0_17","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"229-245","source":"Crossref","is-referenced-by-count":19,"title":["Specification and Checking of Software Contracts for Conditional Information Flow"],"prefix":"10.1007","author":[{"given":"Torben","family":"Amtoft","sequence":"first","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"given":"Edwin","family":"Rodr\u00edguez","sequence":"additional","affiliation":[]},{"family":"Robby","sequence":"additional","affiliation":[]},{"given":"Jonathan","family":"Hoag","sequence":"additional","affiliation":[]},{"given":"David","family":"Greve","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: 33rd Principles of Programming Languages (POPL), pp. 91\u2013102 (2006)","DOI":"10.1145\/1111320.1111046"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Banerjee, A.: Information Flow Analysis in Logical Form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 100\u2013115. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-27864-1_10"},{"issue":"1","key":"17_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2006.03.002","volume":"64","author":"T. Amtoft","year":"2007","unstructured":"Amtoft, T., Banerjee, A.: A logic for information flow analysis with an application to forward slicing of simple imperative programs. Science of Comp. Prog.\u00a064(1), 3\u201328 (2007)","journal-title":"Science of Comp. Prog."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: 5th ACM Workshop on Formal Methods in Security Engineering (FMSE), pp. 2\u201311 (2007); A long version, with proofs, appears as technical report KSU CIS TR 2007-2","DOI":"10.1145\/1314436.1314438"},{"key":"17_CR5","unstructured":"Amtoft, T., Hatcliff, J., Rodriguez, E., Robby, Hoag, J., Greve, D.: Specification and checking of software contracts for conditional information flow (extended version). Technical Report SAnToS-TR2007-5, KSU CIS (2007), http:\/\/www.sireum.org"},{"issue":"15","key":"17_CR6","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"2","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. Journal of Functional Programming\u00a02(15), 131\u2013177 (2005)","journal-title":"Journal of Functional Programming"},{"key":"17_CR7","unstructured":"Barnes, J.: High Integrity Software \u2013 the SPARK Approach to Safety and Security. Addison-Wesley, Reading (2003)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Foccardi, R. (ed.) CSFW 2004, pp. 100\u2013114. IEEE Press, Los Alamitos (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"issue":"1","key":"17_CR9","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"J.-F. Bergeretti","year":"1985","unstructured":"Bergeretti, J.-F., Carr\u00e9, B.A.: Information-flow and data-flow analysis of while-programs. ACM TOPLAS\u00a07(1), 37\u201361 (1985)","journal-title":"ACM TOPLAS"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Chapman, R., Hilton, A.: Enforcing security and safety models with an information flow analysis tool. In: SIGAda 2004, Atlanta, Georgia, November 2004, pp. 39\u201346. ACM, New York (2004)","DOI":"10.1145\/1046191.1032305"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"17_CR13","unstructured":"Greve, D., Wilding, M., Vanfleet, W.M.: A separation kernel formal security policy. In: 4th International Workshop on the ACL2 Prover and its Applications (ACL2-2003) (2003)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C.L., Archer, M., Leonard, E.I., McLean, J.: Formal specification and verification of data separation in a separation kernel for an embedded system. In: 13th ACM Conference on Computer and Communications Security (CCS 2006), pp. 346\u2013355 (2006)","DOI":"10.1145\/1180405.1180448"},{"key":"17_CR15","unstructured":"Jackson, D., Thomas, M., Millett, L.I. (eds.): Software for Dependable Systems: Sufficient Evidence? National Academies Press, Washington (2007); Committee on Certifiably Dependable Software Systems, National Research Council"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: Practical mostly-static information flow control. In: POPL 1999, San Antonio, Texas, pp. 228\u2013241. ACM Press, New York (1999)","DOI":"10.1145\/292540.292561"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Naumann, J.D.A.: From Coupling Relations to Mated Invariants for Checking Information Flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 279\u2013296. Springer, Heidelberg (2006)","DOI":"10.1007\/11863908_18"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, Springer, Heidelberg (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"17_CR20","unstructured":"Rossebo, B., Oman, P., Alves-Foss, J., Blue, R., Jaszkowiak, P.: Using SPARK-Ada to model and verify a MILS message router. In: Proceedings of the International Symposium on Secure Software Engineering (2006)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Rushby, J.: The design and verification of secure systems. In: 8th ACM Symposium on Operating Systems Principles, vol.\u00a015(5), pp. 12\u201321 (1981)","DOI":"10.1145\/1067627.806586"},{"key":"17_CR22","unstructured":"Simonet, V.: Flow Caml in a nutshell. In: Hutton, G. (ed.) First APPSEM-II workshop, March 2003, pp. 152\u2013165 (2003)"},{"issue":"4","key":"17_CR23","doi-asserted-by":"crossref","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. ACM TOSEM\u00a015(4), 410\u2013457 (2006)","journal-title":"ACM TOSEM"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)","DOI":"10.1007\/11547662_24"},{"key":"17_CR25","unstructured":"Vanfleet, M., Luke, J., Beckwith, R.W., Taylor, C., Calloni, B., Uchenick, G.: MILS: Architecture for high-assurance embedded computing. CrossTalk: The Journal of Defense Software Engineering (August 2005)"},{"issue":"3","key":"17_CR26","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security\u00a04(3), 167\u2013188 (1996)","journal-title":"Journal of Computer Security"},{"key":"17_CR27","unstructured":"Sireum website, http:\/\/www.sireum.org"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,30]],"date-time":"2025-01-30T15:15:41Z","timestamp":1738250141000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540682356","9783540682370"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}