Barthe, Gilles; Courtieu, Pierre; Dufay, Guillaume; Melo de Sousa, Simão Tool-assisted specification and verification of typed low-level languages. (English) Zbl 1107.68027 J. Autom. Reasoning 35, No. 4, 295-354 (2005). MSC: 68N15 68T15 PDFBibTeX XMLCite \textit{G. Barthe} et al., J. Autom. Reasoning 35, No. 4, 295--354 (2005; Zbl 1107.68027) Full Text: DOI
Klein, Gerwin; Strecker, Martin Verified bytecode verification and type-certifying compilation. (English) Zbl 1067.68039 J. Log. Algebr. Program. 58, No. 1-2, 27-60 (2004). MSC: 68N15 68N20 PDFBibTeX XMLCite \textit{G. Klein} and \textit{M. Strecker}, J. Log. Algebr. Program. 58, No. 1--2, 27--60 (2004; Zbl 1067.68039) Full Text: DOI
Siveroni, Igor A. Operational semantics of the Java Card Virtual Machine. (English) Zbl 1073.68673 J. Log. Algebr. Program. 58, No. 1-2, 3-25 (2004). MSC: 68Q55 68N15 PDFBibTeX XMLCite \textit{I. A. Siveroni}, J. Log. Algebr. Program. 58, No. 1--2, 3--25 (2004; Zbl 1073.68673) Full Text: DOI
Klein, Gerwin; Nipkow, Tobias Verified bytecode verifiers. (English) Zbl 1038.68109 Theor. Comput. Sci. 298, No. 3, 583-626 (2003). MSC: 68T15 68N15 PDFBibTeX XMLCite \textit{G. Klein} and \textit{T. Nipkow}, Theor. Comput. Sci. 298, No. 3, 583--626 (2003; Zbl 1038.68109) Full Text: DOI