Proof-carrying code from certified abstract interpretation and fixpoint compression

DOI10.1016/j.tcs.2006.08.012zbMath1153.68354OpenAlexW2016209832MaRDI QIDQ860842

N. E. Zubov

Publication date: 9 January 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.08.012

zbMATH Keywords

theorem provingcomputer securityprogram logicabstract interpretationdata flow analysisJava byte code

Mathematics Subject Classification ID

Related Items (7)

Reusing predicate precision in value analysis ⋮ Modular development of certified program verifiers with a proof assistant, ⋮ Verified software units ⋮ Abstraction-carrying code: a model for mobile code safety ⋮ Program and proof optimizations with type systems ⋮ Structural Abstract Interpretation: A Formal Study Using Coq ⋮ Certification Using the Mobius Base Logic

Uses Software

• Coq
• Octagon
• ASTREE

Cites Work

• Lightweight bytecode verification
• Verified bytecode verifiers.
• A compiled implementation of strong reduction
• A semantic model of types and machine instructions for proof-carrying code
• Oracle-based checking of untrusted software
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Formal certification of a compiler back-end or
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof-carrying code from certified abstract interpretation and fixpoint compression