Treffer: Verified bytecode model checkers

Title:
Verified bytecode model checkers
Authors:
BASIN, David, FRIEDRICH, Stefan, GAWKOWSKI, Marek
Source:
TPHOLs 2002 : theorem proving in higher order logics (Hampton VA, 20-23 August 2002)Lecture notes in computer science. :47-66
Publisher Information:
Berlin: Springer, 2002.
Publication Year:
2002
Physical Description:
print, 19 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 programmation, Programming theory, Analyse flux donnée, Data flow analysis, Comportement programme, Program behavior, Comportamiento programa, Langage JAVA, JAVA language, Lenguaje JAVA, Logique temporelle, Temporal logic, Lógica temporal, Machine virtuelle, Virtual machine, Máquina virtual, Modèle logique, Logic model, Modelo lógico, Théorie type, Type theory, Vérification programme, Program verification, Verificación programa, Logique ordre supérieur, High order logic, Vérification modèle, Model checking
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Albert-Ludwigs-Universität Freiburg, Germany
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14636032
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
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14636032
Database:
PASCAL Archive

Weitere Informationen

We have used Isabelle/HOL to formalize and prove correct an approach to bytecode verification based on model checking that we have developed for the Java Virtual Machine. Our work builds on, and extends, the formalization of the Java Virtual Machine and data flow analysis framework of Pusch and Nipkow. By building on their framework, we can reuse their results that relate the run-time behavior of programs with the existence of well-typings for the programs. Our primary extensions are to handle polyvariant data flow analysis and its realization as temporal logic model checking. Aside from establishing the correctness of our model-checking approach, our work contributes to understanding the interrelationships between classical data flow analysis and program analysis based on model checking.