Deciding floating-point logic with abstract conflict driven clause learning
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1948394
- A three-tier strategy for reasoning about floating-point numbers in SMT
- Synthesis of Rigorous Floating-Point Predicates
- Exploiting binary floating-point representations for constraint propagation
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Conflict-driven XOR-clause learning
- Learning from conflicts in propositional satisfiability
- Deciding Bit-Vector Arithmetic with Abstraction
- scientific article; zbMATH DE number 2087547
- scientific article; zbMATH DE number 67109
Cites work
- A machine program for theorem-proving
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
- Abstract conflict driven learning
- Abstract satisfaction
- An abstract domain to discover interval linear equalities
- An abstract interpretation of DPLL(T)
- Anatomy and empirical evaluation of modern SAT solvers
- Computer Aided Verification
- Computer Aided Verification
- Cutting to the chase. Solving linear integer arithmetic
- Floating-point arithmetic in the Coq system
- Formal verification of square root algorithms
- Generalizing DPLL and satisfiability for equalities
- Generalizing DPLL to Richer Logics
- GRASP: a search algorithm for propositional satisfiability
- Handbook of Floating-Point Arithmetic
- scientific article; zbMATH DE number 1670752 (Why is no real title available?)
- scientific article; zbMATH DE number 2084728 (Why is no real title available?)
- scientific article; zbMATH DE number 1832227 (Why is no real title available?)
- scientific article; zbMATH DE number 1863384 (Why is no real title available?)
- scientific article; zbMATH DE number 5263038 (Why is no real title available?)
- Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
- Interval slopes as a numerical abstract domain for floating-point variables
- Multi-prover verification of floating-point programs
- Natural domain SMT: a preliminary assessment
- Numeric bounds analysis with conflict-driven learning
- Program analysis via satisfiability modulo path programs
- Programming Languages and Systems
- Programming Languages and Systems
- Solving non-linear arithmetic
- Splitting on Demand in SAT Modulo Theories
- The MathSAT5 SMT solver
- The reduced product of abstract domains and the combination of decision procedures
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(21)- raSAT: an SMT solver for polynomial constraints
- Exploring approximations for floating-point arithmetic using UppSAT
- Optimization modulo the theories of signed bit-vectors and floating-point numbers
- An SMT theory of fixed-point arithmetic
- Correct approximation of IEEE 754 floating-point arithmetic for program verification
- A three-tier strategy for reasoning about floating-point numbers in SMT
- A two-phase approach for conditional floating-point verification
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Optimization modulo the theory of floating-point numbers
- Abstract interpretation as automated deduction
- An approximation framework for solvers and decision procedures
- A survey of satisfiability modulo theory
- Semantically-guided goal-sensitive reasoning: model representation
- Numeric bounds analysis with conflict-driven learning
- Abstract Interpretation as Automated Deduction
- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
- scientific article; zbMATH DE number 2084728 (Why is no real title available?)
- Lifting CDCL to template-based abstract domains for program verification
- Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Invertibility conditions for floating-point formulas
This page was built for publication: Deciding floating-point logic with abstract conflict driven clause learning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q479837)
