Semantics of roundoff error propagation in finite precision calculations
We introduce a concrete semantics for floating-point operations which describes the propagation of roundoff errors throughout a calculation. This semantics is used to assert the correctness of a static analysis which can be straightforwardly derived ...
The octagon abstract domain
This article presents the octagon abstract domain , a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form X Y c where X and Y range among program ...
Dynamic state restoration using versioning exceptions
We explore the semantics and analysis of a new kind of control structure called a versioning exception that ensures the state of the program, at the point when an exception handler is invoked, reflects the program state at the point when the handler ...
Polymorphic typed defunctionalization and concretization
Defunctionalization is a program transformation that eliminates functions as first-class values. We show that defunctionalization can be viewed as a type-preserving transformation of an extension of F with guarded algebraic data types into ...