Exploring approximations for floating-point arithmetic using UppSAT

DOI10.1007/978-3-319-94205-6_17MaRDI QIDQ1799086zbMATH OpenOpenAlexFDO

Authors Aleksandar Zeljić, Peter Backeman, Christoph M. Wintersteiger, Philipp Rümmer

Publication date 18 October 2018

Full work available at URL https://arxiv.org/abs/1711.08859

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• An approximation framework for solvers and decision procedures
• Deciding floating-point logic with abstract conflict driven clause learning
• Approximations for Model Construction
• On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
• A three-tier strategy for reasoning about floating-point numbers in SMT

Cited in

(5)

• Optimization modulo the theories of signed bit-vectors and floating-point numbers
• An SMT theory of fixed-point arithmetic
• A three-tier strategy for reasoning about floating-point numbers in SMT
• Optimization modulo the theory of floating-point numbers
• An approximation framework for solvers and decision procedures

Describes a project that uses

Uses Software

• MathSAT5
• Coq
• ASTREE
• UppSAT
• XSat
• SONOLAR
• Gappa
• z3
• HOL Light
• dReal

This page was built for publication: Exploring approximations for floating-point arithmetic using UppSAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799086)