Iranmanesh, Zeinab; Fallah, Mehran S. Specification and static enforcement of scheduler-independent noninterference in a middleweight Java. (English) Zbl 1387.68050 Comput. Lang. Syst. Struct. 46, 20-43 (2016). MSC: 68N15 68N19 PDFBibTeX XMLCite \textit{Z. Iranmanesh} and \textit{M. S. Fallah}, Comput. Lang. Syst. Struct. 46, 20--43 (2016; Zbl 1387.68050) Full Text: DOI
Amir-Mohammadian, Sepehr; Fallah, Mehran S. Noninterference in a predicative polymorphic calculus for access control. (English) Zbl 1308.68026 Comput. Lang. Syst. Struct. 39, No. 3, 109-120 (2013). MSC: 68N15 68N18 68Q55 PDFBibTeX XMLCite \textit{S. Amir-Mohammadian} and \textit{M. S. Fallah}, Comput. Lang. Syst. Struct. 39, No. 3, 109--120 (2013; Zbl 1308.68026) Full Text: DOI
Almeida, J. Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara Formal verification of side-channel countermeasures using self-composition. (English) Zbl 1284.68158 Sci. Comput. Program. 78, No. 7, 796-812 (2013). MSC: 68N30 68Q60 94A60 PDFBibTeX XMLCite \textit{J. B. Almeida} et al., Sci. Comput. Program. 78, No. 7, 796--812 (2013; Zbl 1284.68158) Full Text: DOI
Barthe, Gilles; Pichardie, David; Rezk, Tamara A certified lightweight non-interference Java bytecode verifier. (English) Zbl 1282.68089 Math. Struct. Comput. Sci. 23, No. 5, 1032-1081 (2013). MSC: 68N15 PDFBibTeX XMLCite \textit{G. Barthe} et al., Math. Struct. Comput. Sci. 23, No. 5, 1032--1081 (2013; Zbl 1282.68089) Full Text: DOI
Beringer, Lennart Relational decomposition. (English) Zbl 1342.68070 Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 39-54 (2011). MSC: 68N30 03B70 68T15 PDFBibTeX XMLCite \textit{L. Beringer}, Lect. Notes Comput. Sci. 6898, 39--54 (2011; Zbl 1342.68070) Full Text: DOI
Borgström, Johannes; Gordon, Andrew D.; Pucella, Riccardo Roles, stacks, histories: a triple for Hoare. (English) Zbl 1220.68044 J. Funct. Program. 21, No. 2, 159-207 (2011). MSC: 68N18 03B70 68N30 PDFBibTeX XMLCite \textit{J. Borgström} et al., J. Funct. Program. 21, No. 2, 159--207 (2011; Zbl 1220.68044) Full Text: DOI
Beringer, Lennart Relational bytecode correlations. (English) Zbl 1204.68070 J. Log. Algebr. Program. 79, No. 7, 483-514 (2010). MSC: 68N99 PDFBibTeX XMLCite \textit{L. Beringer}, J. Log. Algebr. Program. 79, No. 7, 483--514 (2010; Zbl 1204.68070) Full Text: DOI
Kammüller, Florian Formalizing non-interference for a simple bytecode language in Coq. (English) Zbl 1151.68633 Formal Asp. Comput. 20, No. 3, 259-275 (2008). MSC: 68T15 68N15 68N99 PDFBibTeX XMLCite \textit{F. Kammüller}, Formal Asp. Comput. 20, No. 3, 259--275 (2008; Zbl 1151.68633) Full Text: DOI
Naumann, David A. Observational purity and encapsulation. (English) Zbl 1116.68052 Theor. Comput. Sci. 376, No. 3, 205-224 (2007). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. A. Naumann}, Theor. Comput. Sci. 376, No. 3, 205--224 (2007; Zbl 1116.68052) Full Text: DOI
Naumann, David A.; Barnett, Mike Towards imperative modules: reasoning about invariants and sharing of mutable state. (English) Zbl 1118.68088 Theor. Comput. Sci. 365, No. 1-2, 143-168 (2006). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. A. Naumann} and \textit{M. Barnett}, Theor. Comput. Sci. 365, No. 1--2, 143--168 (2006; Zbl 1118.68088) Full Text: DOI