An approximation framework for solvers and decision procedures

DOI10.1007/s10817-016-9393-1zbMath1409.68265OpenAlexW2551482414WikidataQ59611994 ScholiaQ59611994MaRDI QIDQ2362497

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

Publication date: 10 July 2017

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://europepmc.org/articles/pmc6109943

Mathematics Subject Classification ID

Related Items

Optimization modulo the theories of signed bit-vectors and floating-point numbers

Uses Software

• Coq
• Gappa
• z3
• HOL Light
• dReal
• MathSAT5
• ASTREE
• RAReQS

Cites Work

• Unnamed Item
• Unnamed Item
• Deciding floating-point logic with abstract conflict driven clause learning
• Floating-point arithmetic in the Coq system
• A theory of abstraction
• Solving QBF with Counterexample Guided Refinement
• Numeric Bounds Analysis with Conflict-Driven Learning
• Abstract conflict driven learning
• Certification of bounds on expressions involving rounded operators
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Combining Coq and Gappa for Certifying Floating-Point Programs
• The Strategy Challenge in SMT Solving
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Programming Languages and Systems
• The MathSAT5 SMT Solver
• Deciding Bit-Vector Arithmetic with Abstraction