Applied Mathematics

4 files

1. 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 down-sets 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.
   

   116 downloads

   0 comments

   Updated February 14, 2020

2. Bit-Precise 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 bit-precise 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 so-called 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 anti-unification. The speed and precision of both algorithms are compared on benchmark circuits, to draw conclusions on the tractability of affine abstraction.
   

   96 downloads

   0 comments

   Updated February 14, 2020

3. 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 bit-blasting. This approach is entirely automatic, avoids complicated elimination algorithms, and provides a systematic way of handling wrap-arounds (integer over-flows and underflows) which arise in machine arithmetic.
   

   100 downloads

   0 comments

   Updated February 14, 2020

4. 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).
   

   181 downloads

   0 comments

   Updated February 14, 2020