Aleksandar Zeljic: From machine arithmetic to approximations and back again

PRACTICALITIES

Lunch is served at 12:00 noon (register at tinyurl.com/TCS180322  at the latest on Tuesday morning, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.

ABSTRACT

Safety-critical systems, especially those found in avionics and automotive industries, rely on machine arithmetic to perform their tasks: integer arithmetic, fixed-point arithmetic or floating-point arithmetic (FPA). Machine arithmetic exhibits subtle differences in behavior compared to the ideal mathematical arithmetic, which can make it tricky to use correctly. To show correctness, we formally prove properties of safety-critical systems, which requires reasoning about machine arithmetic. However, scalability is a challenge for existing SMT techniques for machine arithmetic. In this talk, we present two novel techniques aimed at improving the scalability of SMT for machine arithmetic.

First, we present a novel method to reason about the theory of fixed-width bit-vectors called mcBV. It is an instantiation of the model-constructing satisfiability calculus, mcSAT, and uses a new lazy representation of bit-vectors that allows both bit- and word-level reasoning. It uses a greedy explanation generalization mechanism capable of more general learning compared to traditional approaches. Evaluation of mcBV shows that it can outperform bit-blasting on several classes of problems.

Second, we present an approximation-based technique for augmenting existing decision procedures. A general approximation refinement framework is presented, along with its implementation called UppSAT. The framework solves a sequence of approximations. Initially very crude, these approximations are typically very easy to solve. Results of solving approximate constraints are used to either reconstruct a solution of original constraints, obtain a proof of unsatisfiability or to refine the approximation. The framework preserves soundness, completeness, and termination of the underlying decision procedure, guaranteeing that eventually, either a solution is found or a proof that solution does not exist. We present results on the impact of approximations implemented in the UppSAT framework on the state-of-the-art in SMT for floating-point arithmetic.