Verified bytecode verification and type-certifying compilation
type: Item
instance of: scholarly article
title: Verified bytecode verification and type-certifying compilation
zbMATH Open document ID: 1067.68039
author: Gerwin Klein
author: Martin Strecker
published in: The Journal of Logic and Algebraic Programming
publication date: 2004-10-14T00:00:00Z
Mathematics Subject Classification ID: 68N15
Mathematics Subject Classification ID: 68N20
zbMATH DE Number: 2107869
zbMATH Keywords: Java
zbMATH Keywords: JVM
zbMATH Keywords: Compiler
zbMATH Keywords: Bytecode verification
zbMATH Keywords: Theorem proving
describes a project that uses: TALx86
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
full work available at URL: j.jlap.2003.07.004
OpenAlex ID: W2020763704
cites work: Q2763680
cites work: Q4736986
cites work: Q4484331
cites work: Q3122694
cites work: Q4736387
cites work: Q4474214
cites work: Q4222945
cites work: Verified bytecode verifiers.
cites work: Verified lightweight bytecode verification
cites work: Q4553258
cites work: Java bytecode verification: Algorithms and formalizations
cites work: Q4417787
cites work: Q5574395
cites work: Q2769440
cites work: Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
cites work: \(\mu\)Java: Embedding a programming language in a theorem prover
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Hoare logic for Java in Isabelle/HOL
cites work: Q4818817
cites work: Q2742791
cites work: Q4809043
cites work: Q4428314
DOI: 10.1016/J.JLAP.2003.07.004
description: scientific article; zbMATH DE number 2107869