Small Witnesses for Abstract Interpretation-Based Proofs

DOI10.1007/978-3-540-71316-6_19zbMATH Open1187.68146OpenAlexW1575875253MaRDI QIDQ5756500FDOQ5756500

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

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.

Mathematics Subject Classification ID

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

Cited In (4)

• \(\mathrm{PART}_{\mathrm{PW}}\): from partial analysis results to a proof witness
• Title not available (Why is that?)
• 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)