Refinement to certify abstract interpretations: illustrated on linearization for polyhedra

DOI10.1007/s10817-018-9492-2zbMath1465.68047OpenAlexW2899860906MaRDI QIDQ1739912

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)

Uses Software

• Coq
• Verasco

Cites Work

• Unnamed Item
• The Bernstein polynomial basis: a centennial retrospective
• Representing polynomials by positive linear functions on compact convex polyhedra
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Deciding Kleene Algebras in Coq
• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
• Affine Arithmetic and Applications to Real-Number Proving
• Grammar Analysis and Parsing by Abstract Interpretation
• Intuitionistic Refinement Calculus
• Guarded commands, nondeterminacy and formal derivation of programs
• Programming Languages and Systems
• Theorem Proving in Higher Order Logics
• Verification, Model Checking, and Abstract Interpretation