Treffer: Verified bytecode verifiers
Title:
Verified bytecode verifiers
Authors:
Source:
Foundations of Software Science and Computation StructuresTheoretical computer science. 298(3):583-626
Publisher Information:
Amsterdam: Elsevier, 2003.
Publication Year:
2003
Physical Description:
print, 24 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie des langages et analyse syntaxique, Language theory and syntactical analysis, Automates. Machines abstraites. Machines de turing, Automata. Abstract machines. Turing machines, Théorie programmation, Programming theory, Logiciel, Software, Langages de programmation, Programming languages, Démonstration théorème, Theorem proving, Demostración teorema, Flexibilité, Flexibility, Flexibilidad, Informatique théorique, Computer theory, Informática teórica, Langage formel, Formal language, Lenguaje formal, Machine abstraite, Abstract machine, Máquina abstracta, Machine virtuelle, Virtual machine, Máquina virtual, Relation ordre partiel, Partial ordering, Relación orden parcial, Sémantique opérationnelle, Operational semantics, Semantica operacional, Analyse flot donnée, Data flow analysis, Análisis Bayes, Initialisation objet, Object initialization, Vérification bytecode, Bytecode verification
Document Type:
Konferenz
Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Institut für Informatik, Technische Unirersität München, Boltzsmannstr. 3, 80290 München, Germany
ISSN:
0304-3975
Rights:
Copyright 2003 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14647975
Database:
PASCAL Archive
Weitere Informationen
Using the theorem prover Isabelle/HOL we have formalized and proved correct and executable bytecode verifier in the style of Kildall's algorithm for a significant subset of the Java Virtual Machine (JVM). First an abstract framework for proving correctness of data flow based type inference algorithms for assembly languages is formalized. It is shown that under certain conditions Kildall's algorithm yields a correct bytecode verifier. Then the framework is instantiated with our previous work about the JVM. Finally, we demonstrate the flexibility of the framework by extending our previous JVM model and the executable bytecode verifier with object initialization.