Proof-carrying code from certified abstract interpretation and fixpoint compression

DOI10.1016/J.TCS.2006.08.012MaRDI QIDQ860842zbMATH OpenOpenAlexFDO

Authors 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

abstract interpretationtheorem provingprogram logiccomputer securitydata flow analysisJava byte code

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Abstraction-carrying code: a model for mobile code safety
• Logic for Programming, Artificial Intelligence, and Reasoning
• scientific article; zbMATH DE number 2110618
• Logic Programming
• scientific article; zbMATH DE number 2090287

Cites work

• scientific article; zbMATH DE number 2163030 (Why is no real title available?)
• scientific article; zbMATH DE number 1390341 (Why is no real title available?)
• scientific article; zbMATH DE number 1392299 (Why is no real title available?)
• A compiled implementation of strong reduction
• A semantic model of types and machine instructions for proof-carrying code
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Lightweight bytecode verification
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Oracle-based checking of untrusted software
• Programming Languages and Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Verified bytecode verifiers.

Cited in

(21)

• A portable virtual machine target for proof-carrying code
• Building certified libraries for PCC: dynamic storage allocation
• Abstraction-carrying code: a model for mobile code safety
• scientific article; zbMATH DE number 1956568 (Why is no real title available?)
• Verified software units
• Structural Abstract Interpretation: A Formal Study Using Coq
• Verification, Model Checking, and Abstract Interpretation
• Small Witnesses for Abstract Interpretation-Based Proofs
• Automatic construction of Hoare proofs from abstract interpretation results.
• Program and proof optimizations with type systems
• scientific article; zbMATH DE number 1692889 (Why is no real title available?)
• Modular development of certified program verifiers with a proof assistant,
• Reusing predicate precision in value analysis
• An Incremental Approach to Abstraction-Carrying Code
• scientific article; zbMATH DE number 1956565 (Why is no real title available?)
• scientific article; zbMATH DE number 2110618 (Why is no real title available?)
• Proof-Producing Program Analysis
• Logic for Programming, Artificial Intelligence, and Reasoning
• An Introduction to Certificate Translation
• Certification Using the Mobius Base Logic
• Logic Programming

Describes a project that uses

Uses Software

• ASTREE
• Octagon
• Coq

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

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