Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra

DOI10.1007/978-3-319-22102-1_7zbMath1465.68046OpenAlexW2140960438MaRDI QIDQ2945626

Sylvain Boulmé, Alexandre Maréchal

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_7

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)

Related Items (1)

Refinement to certify abstract interpretations: illustrated on linearization for polyhedra

Uses Software

• Coq

Cites Work

• 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
• Type classes for mathematics in type theory
• Grammar Analysis and Parsing by Abstract Interpretation
• Theorem Proving in Higher Order Logics
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra