Affine Arithmetic

Fabian Immler

7 February 2014

Abstract

We give a formalization of affine forms as abstract representations of zonotopes. We provide affine operations as well as overapproximations of some non-affine operations like multiplication and division. Expressions involving those operations can automatically be turned into (executable) functions approximating the original expression in affine arithmetic.
BSD License

Change history

[2015-01-31] added algorithm for zonotope/hyperplane intersection
[2017-09-20] linear approximations for all symbols from the floatarith data type

Depends On

Used by

Topics

Related Entries

Theories

Cite

×
@article{Affine_Arithmetic-AFP,
  author  = {Fabian Immler},
  title   = {Affine Arithmetic},
  journal = {Archive of Formal Proofs},
  month   = February,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Affine_Arithmetic.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download