Refinement to certify abstract interpretations: illustrated on linearization for polyhedra

DOI10.1007/S10817-018-9492-2MaRDI QIDQ1739912zbMATH OpenOpenAlexWikidataFDO

Authors Sylvain Boulmé, Alexandre Maréchal

Publication date 29 April 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-018-9492-2

zbMATH Keywords

abstract interpretationproof assistantsresult certification

Mathematics Subject Classification ID

Computational aspects related to convexity (52B55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
• Certified Static Analysis by Abstract Interpretation
• A certified denotational abstract interpreter
• Fast polyhedra abstract domain
• Refinements for free!

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• Affine arithmetic and applications to real-number proving
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Deciding Kleene algebras in \texttt{Coq}
• Grammar Analysis and Parsing by Abstract Interpretation
• Guarded commands, nondeterminacy and formal derivation of programs
• Intuitionistic Refinement Calculus
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Programming Languages and Systems
• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
• Representing polynomials by positive linear functions on compact convex polyhedra
• The Bernstein polynomial basis: a centennial retrospective
• Theorem Proving in Higher Order Logics
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra

Describes a project that uses

Uses Software

• Verasco
• Coq

This page was built for publication: Refinement to certify abstract interpretations: illustrated on linearization for polyhedra

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