Theorem proving demonstrates promising potential for verifying problems beyond the capabilities of SMT-solver-based verification tools. We explore and showcase the capability of Lean, an increasingly popular theorem-proving tool, in deriving the error bounds of table-based Logarithmic Number Systems (LNS). LNS reduces the number of bits needed to represent a high dynamic range of real numbers with finite precision and efficiently performs multiplication and division. However, in LNS, addition and subtraction become non-linear functions that must be approximated–typically using precomputed look-up tables. We provide the first rigorous analysis of LNS that covers first-order Taylor approximation, cotransformation techniques in-spired by European Logarithmic Microprocessor, and the errors introduced by fixed-point arithmetic involved in LNS implementations. By analyzing all error sources and deriving symbolic error bounds for each, then accumulating these to obtain the final error bound, we prove the correctness of these bounds using Lean and its Mathlib library. We empirically validate our analysis using an exhaustive Python implementation, demonstrating that our analytical interpolation bounds are tight, and our analytical cotransformation bounds overestimate between one and two bits.

Rigorous estimation of maximum floating-point round-off errors is an important capability central to many formal verification tools. Unfortunately, available techniques for this task often provide very pessimistic overestimates, causing unnecessary verification failure. We have developed a new approach called Symbolic Taylor Expansions that avoids these problems, and implemented a new tool called FPTaylor embodying this approach. Key to our approach is the use of rigorous global optimization, instead of the more familiar interval arithmetic, affine arithmetic, and/or SMT solvers. FPTaylor emits per-instance analysis certificates in the form of HOL Light proofs that can be machine checked. In this article, we present the basic ideas behind Symbolic Taylor Expansions in detail. We also survey as well as thoroughly evaluate six tool families, namely, Gappa (two tool options studied), Fluctuat, PRECiSA, Real2Float, Rosa, and FPTaylor (two tool options studied) on 24 examples, running on the same machine, and taking care to find the best options for running each of these tools. This study demonstrates that FPTaylor estimates round-off errors within much tighter bounds compared to other tools on a significant number of case studies. We also release FPTaylor along with our benchmarks, thus contributing to future studies and tool development in this area.

Virtually all real-valued computations are carried out using floating-point data types and operations. The precision of these data types must be set with the goals of reducing the overall round-off error, but also emphasizing performance improvements. Often, a mixed-precision allocation achieves this optimum; unfortunately, there are no techniques available to compute such allocations and conservatively meet a given error target across all program inputs. In this work, we present a rigorous approach to precision allocation based on formal analysis via Symbolic Taylor Expansions, and error analysis based on interval functions. This approach is implemented in an automated tool called FPTuner that generates and solves a quadratically constrained quadratic program to obtain a precision-annotated version of the given expression. FPTuner automatically introduces all the requisite precision up and down casting operations. It also allows users to flexibly control precision allocation using constraints to cap the number of high precision operators as well as group operators to allocate the same precision to facilitate vectorization. We evaluate FPTuner by tuning several benchmarks and measuring the proportion of lower precision operators allocated as we increase the error threshold. We also measure the reduction in energy consumption resulting from executing mixed-precision tuned code on a real hardware platform. We observe significant energy savings in response to mixed-precision tuning, but also observe situations where unexpected compiler behaviors thwart intended optimizations.

People with spinal cord injury (SCI) are predisposed to pressure ulcers (PU). PU remain a significant burden in cost of care and quality of life despite improved mechanistic understanding and advanced interventions. An agent-based model (ABM) of ischemia/reperfusion-induced inflammation and PU (the PUABM) was created, calibrated to serial images of post-SCI PU, and used to investigate potential treatments in silico. Tissue-level features of the PUABM recapitulated visual patterns of ulcer formation in individuals with SCI. These morphological features, along with simulated cell counts and mediator concentrations, suggested that the influence of inflammatory dynamics caused simulations to be committed to "better" vs. "worse" outcomes by 4 days of simulated time and prior to ulcer formation. Sensitivity analysis of model parameters suggested that increasing oxygen availability would reduce PU incidence. Using the PUABM, in silico trials of anti-inflammatory treatments such as corticosteroids and a neutralizing antibody targeted at Damage-Associated Molecular Pattern molecules (DAMPs) suggested that, at best, early application at a sufficiently high dose could attenuate local inflammation and reduce pressure-associated tissue damage, but could not reduce PU incidence. The PUABM thus shows promise as an adjunct for mechanistic understanding, diagnosis, and design of therapies in the setting of PU.

Tools for floating-point error estimation are fundamental to program understanding and optimization. In this paper, we focus on tools for determining the input settings to a floating point routine that maximizes its result error. Such tools can help support activities such as precision allocation, performance optimization, and auto-tuning. We benchmark current abstraction-based precision analysis methods, and show that they often do not work at scale, or generate highly pessimistic error estimates, often caused by non-linear operators or complex input constraints that define the set of legal inputs. We show that while concrete-testing-based error estimation methods based on maintaining shadow values at higher precision can search out higher error-inducing inputs, suit able heuristic search guidance is key to finding higher errors. We develop a heuristic search algorithm called Binary Guided Random Testing (BGRT). In 45 of the 48 total benchmarks, including many real-world routines, BGRT returns higher guaranteed errors. We also evaluate BGRT against two other heuristic search methods called ILS and PSO, obtaining better results.

Pressure ulcers are costly and life-threatening complications for people with spinal cord injury (SCI). People with SCI also exhibit differential blood flow properties in non-ulcerated skin. We hypothesized that a computer simulation of the pressure ulcer formation process, informed by data regarding skin blood flow and reactive hyperemia in response to pressure, could provide insights into the pathogenesis and effective treatment of post-SCI pressure ulcers. Agent-Based Models (ABM) are useful in settings such as pressure ulcers, in which spatial realism is important. Ordinary Differential Equation-based (ODE) models are useful when modeling physiological phenomena such as reactive hyperemia. Accordingly, we constructed a hybrid model that combines ODEs related to blood flow along with an ABM of skin injury, inflammation, and ulcer formation. The relationship between pressure and the course of ulcer formation, as well as several other important characteristic patterns of pressure ulcer formation, was demonstrated in this model. The ODE portion of this model was calibrated to data related to blood flow following experimental pressure responses in non-injured human subjects or to data from people with SCI. This model predicted a higher propensity to form ulcers in response to pressure in people with SCI vs. non-injured control subjects, and thus may serve as novel diagnostic platform for post-SCI ulcer formation.