{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T00:20:48Z","timestamp":1787530848378,"version":"build-2736575974"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T00:00:00Z","timestamp":1602028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,7]]},"DOI":"10.1145\/3372020.3391565","type":"proceedings-article","created":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T20:02:05Z","timestamp":1599940925000},"page":"44-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Lattice-Based Information Flow Control-by-Construction for Security-by-Design"],"prefix":"10.1145","author":[{"given":"Tobias","family":"Runge","sequence":"first","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Kn\u00fcppel","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[{"name":"University of Ulm, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Modeling in Event-B - System and Software Engineering","author":"Abrial Jean-Raymond","unstructured":"Jean-Raymond Abrial . 2010. Modeling in Event-B - System and Software Engineering . Cambridge University Press . Jean-Raymond Abrial. 2010. Modeling in Event-B - System and Software Engineering. Cambridge University Press."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_3_2_1_3_1","volume-title":"SAS (LNCS)","author":"Amtoft Torben","unstructured":"Torben Amtoft and Anindya Banerjee . 2004. Information Flow Analysis in Logical Form . In SAS (LNCS) , Vol. 3148 . Springer , 100--115. Torben Amtoft and Anindya Banerjee. 2004. Information Flow Analysis in Logical Form. In SAS (LNCS), Vol. 3148. Springer, 100--115."},{"key":"e_1_3_2_1_4_1","volume-title":"Greve","author":"Amtoft Torben","year":"2008","unstructured":"Torben Amtoft , John Hatcliff , Edwin Rodriguez , Robby, Jonathan Hoag , and David A . Greve . 2008 . Specification and Checking of Software Contracts for Conditional Information Flow. In FM. Springer , 229--245. Torben Amtoft, John Hatcliff, Edwin Rodriguez, Robby, Jonathan Hoag, and David A. Greve. 2008. Specification and Checking of Software Contracts for Conditional Information Flow. In FM. Springer, 229--245."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357088"},{"key":"e_1_3_2_1_6_1","volume-title":"Damien Octeau, and Patrick D. McDaniel.","author":"Arzt Steven","year":"2014","unstructured":"Steven Arzt , Siegfried Rasthofer , Christian Fritz , Eric Bodden , Alexandre Bartel , Jacques Klein , Yves Le Traon , Damien Octeau, and Patrick D. McDaniel. 2014 . FlowDroid: Precise Context , Flow, Field, Object-Sensitive and Lifecycle-Aware Taint Analysis for Android Apps. In PLDI, Vol. 49 . ACM , 259--269. Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick D. McDaniel. 2014. FlowDroid: Precise Context, Flow, Field, Object-Sensitive and Lifecycle-Aware Taint Analysis for Android Apps. In PLDI, Vol. 49. ACM, 259--269."},{"key":"e_1_3_2_1_7_1","first-page":"227","article-title":"Invariant Based Programming: Basic Approach and Teaching Experiences","volume":"21","author":"Back Ralph-Johan","year":"2009","unstructured":"Ralph-Johan Back . 2009 . Invariant Based Programming: Basic Approach and Teaching Experiences . FAOC 21 , 3 (2009), 227 -- 244 . Ralph-Johan Back. 2009. Invariant Based Programming: Basic Approach and Teaching Experiences. FAOC 21, 3 (2009), 227--244.","journal-title":"FAOC"},{"key":"e_1_3_2_1_8_1","volume-title":"TAP (LNCS)","author":"Back Ralph-Johan","unstructured":"Ralph-Johan Back , Johannes Eriksson , and Magnus Myreen . 2007. Testing and Verifying Invariant Based Programs in the SOCOS Environment . In TAP (LNCS) , Vol. 4454 . Springer , 61--78. Ralph-Johan Back, Johannes Eriksson, and Magnus Myreen. 2007. Testing and Verifying Invariant Based Programs in the SOCOS Environment. In TAP (LNCS), Vol. 4454. Springer, 61--78."},{"key":"e_1_3_2_1_9_1","volume-title":"Refinement Calculus: A Systematic Introduction","author":"Back Ralph-Johan","year":"2012","unstructured":"Ralph-Johan Back and Joakim Wright . 2012 . Refinement Calculus: A Systematic Introduction . Springer Science & Business Media . Ralph-Johan Back and Joakim Wright. 2012. Refinement Calculus: A Systematic Introduction. Springer Science & Business Media."},{"key":"e_1_3_2_1_10_1","first-page":"253","article-title":"Secure Information Flow and Pointer Confinement in a Java-like Language","volume":"2","author":"Banerjee Anindya","year":"2002","unstructured":"Anindya Banerjee and David A Naumann . 2002 . Secure Information Flow and Pointer Confinement in a Java-like Language .. In CSFW , Vol. 2. 253 . Anindya Banerjee and David A Naumann. 2002. Secure Information Flow and Pointer Confinement in a Java-like Language.. In CSFW, Vol. 2. 253.","journal-title":"CSFW"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA023588"},{"key":"e_1_3_2_1_13_1","first-page":"1152","article-title":"On the Secure Software Development Process: CLASP, SDL and Touchpoints Compared","volume":"51","author":"Win Bart De","year":"2009","unstructured":"Bart De Win , Riccardo Scandariato , Koen Buyens , Johan Gr\u00e9goire , and Wouter Joosen . 2009 . On the Secure Software Development Process: CLASP, SDL and Touchpoints Compared . InfSof 51 , 7 (2009), 1152 -- 1171 . Bart De Win, Riccardo Scandariato, Koen Buyens, Johan Gr\u00e9goire, and Wouter Joosen. 2009. On the Secure Software Development Process: CLASP, SDL and Touchpoints Compared. InfSof 51, 7 (2009), 1152--1171.","journal-title":"InfSof"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_3_2_1_15_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice Hall . Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall."},{"key":"e_1_3_2_1_16_1","volume-title":"U Chapter, U Why In, U First Steps, U New Threats, U Windows, U Seeking Scalability, et al.","author":"Howard Michael","year":"2006","unstructured":"Michael Howard , Steve Lipner , U Index , U Part , U Chapter, U Why In, U First Steps, U New Threats, U Windows, U Seeking Scalability, et al. 2006 . The Security Development Lifecycle: SDL : A Process for Developing Demonstrably More Secure Software. Microsoft Press . Michael Howard, Steve Lipner, U Index, U Part, U Chapter, U Why In, U First Steps, U New Threats, U Windows, U Seeking Scalability, et al. 2006. The Security Development Lifecycle: SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press."},{"key":"e_1_3_2_1_17_1","first-page":"1","article-title":"On Flow-Sensitive Security Types","volume":"41","author":"Hunt Sebastian","year":"2006","unstructured":"Sebastian Hunt and David Sands . 2006 . On Flow-Sensitive Security Types . SIG-PLANNot. 41 , 1 (Jan. 2006), 79--90. Sebastian Hunt and David Sands. 2006. On Flow-Sensitive Security Types. SIG-PLANNot. 41, 1 (Jan. 2006), 79--90.","journal-title":"SIG-PLANNot."},{"key":"e_1_3_2_1_18_1","volume-title":"Watson","author":"Kourie Derrick G.","year":"2012","unstructured":"Derrick G. Kourie and Bruce W . Watson . 2012 . The Correctness-By-Construction Approach to Programming. Springer . Derrick G. Kourie and Bruce W. Watson. 2012. The Correctness-By-Construction Approach to Programming. Springer."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.17"},{"key":"e_1_3_2_1_20_1","volume-title":"Programming from Specifications","author":"Morgan Carroll","unstructured":"Carroll Morgan . 1994. Programming from Specifications ( 2 nd ed.). Prentice Hall . Carroll Morgan. 1994. Programming from Specifications (2nd ed.). Prentice Hall.","edition":"2"},{"key":"e_1_3_2_1_21_1","volume-title":"JFlow: Practical Mostly-Static Information Flow Control","author":"Myers Andrew C.","unstructured":"Andrew C. Myers . 1999. JFlow: Practical Mostly-Static Information Flow Control . ACM , New York, NY, USA , 228--241. Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. ACM, New York, NY, USA, 228--241."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363526"},{"key":"e_1_3_2_1_23_1","volume-title":"Hanne Riis Nielson, and Chris Hankin","author":"Nielson Flemming","year":"1999","unstructured":"Flemming Nielson , Hanne Riis Nielson, and Chris Hankin . 1999 . Principles of Program Analysis. Springer . Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer."},{"key":"e_1_3_2_1_24_1","first-page":"28","article-title":"ArcAngel: A Tactic Language for Refinement","volume":"15","author":"Medeiros Oliveira Marcel Vinicius","year":"2003","unstructured":"Marcel Vinicius Medeiros Oliveira , Ana Cavalcanti , and Jim Woodcock . 2003 . ArcAngel: A Tactic Language for Refinement . FAOC 15 , 1 (2003), 28 -- 47 . Marcel Vinicius Medeiros Oliveira, Ana Cavalcanti, and Jim Woodcock. 2003. ArcAngel: A Tactic Language for Refinement. FAOC 15, 1 (2003), 28--47.","journal-title":"FAOC"},{"key":"e_1_3_2_1_25_1","volume-title":"EASE (LNCS)","author":"Runge Tobias","unstructured":"Tobias Runge , Ina Schaefer , Loek Cleophas , Thomas Th\u00fcm , Derrick Kourie , and Bruce W Watson . 2019. Tool Support for Correctness-by-Construction . In EASE (LNCS) , Vol. 11424 . Springer , 25--42. Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Th\u00fcm, Derrick Kourie, and Bruce W Watson. 2019. Tool Support for Correctness-by-Construction. In EASE (LNCS), Vol. 11424. Springer, 25--42."},{"key":"e_1_3_2_1_26_1","volume-title":"Refine","author":"Runge Tobias","unstructured":"Tobias Runge , Thomas Th\u00fcm , Loek Cleophas , Ina Schaefer , and Bruce W Watson . 2019. Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative User Study . In Refine . Springer . To appear. Tobias Runge, Thomas Th\u00fcm, Loek Cleophas, Ina Schaefer, and Bruce W Watson. 2019. Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative User Study. In Refine. Springer. To appear."},{"key":"e_1_3_2_1_27_1","volume-title":"Static Flow-Sensitive Security Analysis. In 2010 23rd IEEE Computer Security Foundations Symposium. IEEE, 186--199","author":"Russo Alejandro","year":"2010","unstructured":"Alejandro Russo and Andrei Sabelfeld . 2010 . Dynamic vs . Static Flow-Sensitive Security Analysis. In 2010 23rd IEEE Computer Security Foundations Symposium. IEEE, 186--199 . Alejandro Russo and Andrei Sabelfeld. 2010. Dynamic vs. Static Flow-Sensitive Security Analysis. In 2010 23rd IEEE Computer Security Foundations Symposium. IEEE, 186--199."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_29_1","volume-title":"ISoLA (LNCS), Vol 11244","author":"Schaefer Ina","unstructured":"Ina Schaefer , Tobias Runge , Alexander Kn\u00fcppel , Loek Cleophas , Derrick Kourie , and Bruce W Watson . 2018. Towards Confidentiality-by-Construction . In ISoLA (LNCS), Vol 11244 . Springer , 502--515. Ina Schaefer, Tobias Runge, Alexander Kn\u00fcppel, Loek Cleophas, Derrick Kourie, and Bruce W Watson. 2018. Towards Confidentiality-by-Construction. In ISoLA (LNCS), Vol 11244. Springer, 502--515."},{"key":"e_1_3_2_1_30_1","volume-title":"Flaws in Flows: Unveiling Design Flaws via Information Flow Analysis","author":"Turna Katja","unstructured":"Katja Turna , Riccardo Scandariato , and Musard Balliu . 2019. Flaws in Flows: Unveiling Design Flaws via Information Flow Analysis . In ICSA. IEEE , 191--200. Katja Turna, Riccardo Scandariato, and Musard Balliu. 2019. Flaws in Flows: Unveiling Design Flaws via Information Flow Analysis. In ICSA. IEEE, 191--200."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_3_2_1_32_1","volume-title":"ISoLA (LNCS)","author":"Watson Bruce W.","unstructured":"Bruce W. Watson , Derrick G. Kourie , Ina Schaefer , and Loek Cleophas . 2016. Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience? . In ISoLA (LNCS) , Vol. 9952 . Springer , 730--748. Bruce W. Watson, Derrick G. Kourie, Ina Schaefer, and Loek Cleophas. 2016. Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?. In ISoLA (LNCS), Vol. 9952. Springer, 730--748."},{"key":"e_1_3_2_1_33_1","volume-title":"Myers","author":"Zdancewic Steve","year":"2001","unstructured":"Steve Zdancewic and Andrew C . Myers . 2001 . Robust Declassification. In CSFW. IEEE , 15--23. Steve Zdancewic and Andrew C. Myers. 2001. Robust Declassification. In CSFW. IEEE, 15--23."}],"event":{"name":"FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering","location":"Seoul Republic of Korea","acronym":"FormaliSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 8th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391565","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372020.3391565","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:19Z","timestamp":1750203859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391565"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":32,"alternative-id":["10.1145\/3372020.3391565","10.1145\/3372020"],"URL":"https:\/\/doi.org\/10.1145\/3372020.3391565","relation":{},"subject":[],"published":{"date-parts":[[2020,10,7]]},"assertion":[{"value":"2020-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}