Formalizing a JVML verifier for initialization in a theorem prover

DOI10.1007/3-540-44585-4_3MaRDI QIDQ4551130zbMATH OpenFDO

Authors Yves Bertot

Publication date 4 September 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2102/21020014

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Verified bytecode verifiers.
• Verified bytecode verifiers
• Java bytecode verification: Algorithms and formalizations
• scientific article; zbMATH DE number 1231622
• Java bytecode verification: An overview

Cited in

(14)

• Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
• Verified bytecode verifiers.
• Weakest pre-condition reasoning for Java programs with JML annotations
• Formal specification and verification of JDK's identity hash map implementation
• Extracting a data flow analyser in constructive logic
• scientific article; zbMATH DE number 1231622 (Why is no real title available?)
• Java bytecode verification: An overview
• Improving the official specification of Java bytecode verification
• Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Computer Aided Verification
• Reasoning about safety properties in a JVM-like environment

Describes a project that uses

Uses Software

• PVS
• Coq

This page was built for publication: Formalizing a JVML verifier for initialization in a theorem prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4551130)