Proof-Producing Program Analysis

DOI10.1007/11921240_20MaRDI QIDQ3525156zbMATH OpenOpenAlexFDO

Authors Amine Chaieb

Publication date 11 September 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11921240_20

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic construction of Hoare proofs from abstract interpretation results.
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• scientific article; zbMATH DE number 2163030
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 2110618

Cited in

(11)

• Reusing predicate precision in value analysis
• Certifying safety and termination proofs for integer transition systems
• Inter-program Properties
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• \(\mathrm{PART}_{\mathrm{PW}}\): from partial analysis results to a proof witness
• Certificate Translation in Abstract Interpretation
• Automatic construction of Hoare proofs from abstract interpretation results.
• Analyzing mathematical programs using MProbe
• Program analysis is harder than verification: a computability perspective
• Proof optimization for partial redundancy elimination
• Formal proof of a program: find

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Proof-Producing Program Analysis

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