Verified bytecode verifiers
From MaRDI portal
Recommendations
Cited in
(30)- A type system for the Java bytecode language and verifier
- Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
- Verified bytecode subroutines
- Bytecode verification by model checking
- Introduction to ``Milestones in interactive theorem proving
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Lightweight bytecode verification
- A type system for JVM threads
- Verified bytecode verifiers.
- Verified bytecode verification and type-certifying compilation
- Java: Embedding a programming language in a theorem prover
- Verified lightweight bytecode verification
- scientific article; zbMATH DE number 1927414 (Why is no real title available?)
- scientific article; zbMATH DE number 1796120 (Why is no real title available?)
- scientific article; zbMATH DE number 2087621 (Why is no real title available?)
- Computer Science Logic
- Programming Languages and Systems
- A Bytecode Logic for JML and Types
- A certified lightweight non-interference Java bytecode verifier
- Fundamental Approaches to Software Engineering
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Computer Aided Verification
- Types for Proofs and Programs
- Java's integral types in PVS.
- \textsc{Mnemonics}: type-safe bytecode generation at run time
- Relational bytecode correlations
- Proving total correctness of top-down solvers with widening and narrowing
- Tool-assisted specification and verification of typed low-level languages
- A new type system for JVM lock primitives
This page was built for publication: Verified bytecode verifiers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2769440)
