Small Witnesses for Abstract Interpretation-Based Proofs

DOI10.1007/978-3-540-71316-6_19MaRDI QIDQ5756500zbMATH OpenOpenAlexFDO

Authors

Publication date 4 September 2007

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71316-6_19

Mathematics Subject Classification ID

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

Recommendations

• Certificate size reduction in abstraction-carrying code
• Reduced Certificates for Abstraction-Carrying Code
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Logic for Programming, Artificial Intelligence, and Reasoning
• Automatic construction of Hoare proofs from abstract interpretation results.

Cited in

(4)

• \(\mathrm{PART}_{\mathrm{PW}}\): from partial analysis results to a proof witness
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• When are software verification results valid for approximate hardware?
• Logic Programming

This page was built for publication: Small Witnesses for Abstract Interpretation-Based Proofs

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