Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
type: Item
instance of: scholarly article
title: Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
zbMATH Open document ID: 1465.68047
author: Sylvain Boulmé
author: Alexandre Maréchal
published in: Journal of Automated Reasoning
publication date: 2019-04-29T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 52B55
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 7048642
zbMATH Keywords: proof assistants
zbMATH Keywords: result certification
zbMATH Keywords: abstract interpretation
describes a project that uses: Verasco
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: s10817-018-9492-2
OpenAlex ID: W2899860906
cites work: Intuitionistic Refinement Calculus
cites work: Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
cites work: Deciding Kleene algebras in \texttt{Coq}
cites work: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
cites work: Grammar Analysis and Parsing by Abstract Interpretation
cites work: Guarded commands, nondeterminacy and formal derivation of programs
cites work: The Bernstein polynomial basis: a centennial retrospective
cites work: Theorem Proving in Higher Order Logics
cites work: Representing polynomials by positive linear functions on compact convex polyhedra
cites work: Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
cites work: Programming Languages and Systems
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Q4301161
cites work: Affine Arithmetic and Applications to Real-Number Proving
DOI: 10.1007/S10817-018-9492-2
Wikidata QID: Q128953437
description: scientific article; zbMATH DE number 7048642