FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
The next 10^4 UppSAT Approximations

Authors: Peter Backeman, Aleksandar Zeljić, Philipp Ruemmer and Christoph M. Wintersteiger

Paper Information

Title:The next 10^4 UppSAT Approximations
Authors:Peter Backeman, Aleksandar Zeljić, Philipp Ruemmer and Christoph M. Wintersteiger
Proceedings:SMT Informal Proceedings
Editors: Rayna Dimitrova and Vijay D'Silva
Keywords:SMT, Approximation, Floating Point Arithmetic, Fixed Point Arithmetic, Linearization, Real Arithetmic
Abstract:

ABSTRACT. Reasoning about complex SMT theories is still quite challenging, for instance bit-vectors, floating-point arithmetic, or strings. Approximations offer a means of mapping a complex theory into a simpler one, and attempting to reconstruct models or proofs in the original theory afterwards. UppSAT is an approximating abstract SMT-solver, based on the systematic approximation refinement framework. The framework can be instantiated using an approximation and a back-end SMT solver. Implemented in Scala, UppSAT is designed with easy and flexible specification of approximations in mind. We discuss the structure of approximations in UppSAT and the components needed for their specification. Because approximation components can be defined relatively independently, they can be flexibly combined to obtain many different flavours of approximation. In this extended abstract we discuss what kinds of approximations can be expressed in UppSAT, along with design choices that enable the modular mix-and-match specification of approximations. Finally, we also outline ideas for several new approximations and strategies which we are currently working on (with first results expected to be available at the workshop).

Pages:6
Talk:Jul 12 11:30 (Session 74F)
Paper: