Applied Mathematics
Mathematics, algorithms and machine arithmetic...
4 files

Lattice Duality: The Origin of Probability and Entropy
By Teddy Rogers
Bayesian probability theory is an inference calculus, which originates from a generalization of inclusion on the Boolean lattice of logical assertions to a degree of inclusion represented by a real number. Dual to this lattice is the distributive lattice of questions constructed from the ordered set of downsets of assertions, which forms the foundation of the calculus of inquiryâ€”a generalization of information theory. In this paper we introduce this novel perspective on these spaces in which machine learning is performed and discuss the relationship between these results and several proposed generalizations of information theory in the literature.
119 downloads
0 comments
Updated

BitPrecise Reasoning with Affine Functions
By Teddy Rogers
The class of affine Boolean functions is rich enough to express constant bits and dependencies between different bits of different words. For example, the function is affine and expresses the invariant that the low bit (bit 0) of the variable x is true, that bit 1 of y is false, that the bits 4 and 7 of x and y coincide whereas bits 5 and 9 of x and y differ. This class of Boolean function is amenable to bitprecise reasoning since it satisfies strong chain properties which bound the number of times a system of semantic fixpoint equations need to be reapplied when reasoning about loops. This paper address the key problem of abstracting an arbitrary Boolean function to either a general affine function or a socalled affine function of width 2, when the function is represented as an ROBDD. Novel algorithms are presented for this task: one that manipulates Boolean vectors and another which is inspired by antiunification. The speed and precision of both algorithms are compared on benchmark circuits, to draw conclusions on the tractability of affine abstraction.
99 downloads
0 comments
Updated

Automatic Abstraction for Intervals Using Boolean Formulae
By Teddy Rogers
Traditionally, transfer functions have been manually designed for each operation in a program. Recently, however, there has been growing interest in computing transfer functions, motivated by the desire to reason about sequences of operations that constitute basic blocks. This paper focuses on deriving transfer functions for intervals â€” possibly the most widely used numeric domain â€” and shows how they can be computed from Boolean formulae which are derived through bitblasting. This approach is entirely automatic, avoids complicated elimination algorithms, and provides a systematic way of handling wraparounds (integer overflows and underflows) which arise in machine arithmetic.
102 downloads
0 comments
Updated

Applied Mathematics for Reversers
By Teddy Rogers
An introduction into modular arithmetics and where to use it. This is the last essay about modular arithmetics, about the Extended Euclidean Algorithm for modular multiplicative inverse calculation and finally about the Chinese Remainder Rheorem (CRT).
187 downloads
0 comments
Updated

Download Statistics
2,105
Files228
Comments894
Reviews