Deciding floating-point logic with abstract conflict driven clause learning (Q479837): Difference between revisions

@@ Property / DOI @@
-.1007/s10703-013-0203-7
@@ Property / DOI: 10.1007/s10703-013-0203-7 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+CBMC
@@ Property / describes a project that uses: CBMC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MathSAT5
@@ Property / describes a project that uses: MathSAT5 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ASTREE
@@ Property / describes a project that uses: ASTREE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SONOLAR
@@ Property / describes a project that uses: SONOLAR / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10703-013-0203-7
+Normal rank
@@ Property / OpenAlex ID @@
+W2127145687
@@ Property / OpenAlex ID: W2127145687 / rank @@
+Normal rank
@@ Property / cites work @@
+Multi-Prover Verification of Floating-Point Programs
+Normal rank
@@ Property / cites work @@
+Generalizing DPLL and satisfiability for equalities
+Normal rank
@@ Property / cites work @@
+Splitting on Demand in SAT Modulo Theories
@@ Property / cites work: Splitting on Demand in SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+An Abstract Interpretation of DPLL(T)
@@ Property / cites work: An Abstract Interpretation of DPLL(T) / rank @@
+Normal rank
@@ Property / cites work @@
+Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables
+Normal rank
@@ Property / cites work @@
+Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
+Normal rank
@@ Property / cites work @@
+An Abstract Domain to Discover Interval Linear Equalities
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Natural Domain SMT: A Preliminary Assessment
@@ Property / cites work: Natural Domain SMT: A Preliminary Assessment / rank @@
+Normal rank
@@ Property / cites work @@
+The Reduced Product of Abstract Domains and the Combination of Decision Procedures
+Normal rank
@@ Property / cites work @@
+Q4790659
@@ Property / cites work: Q4790659 / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+Numeric Bounds Analysis with Conflict-Driven Learning
+Normal rank
@@ Property / cites work @@
+Abstract conflict driven learning
@@ Property / cites work: Abstract conflict driven learning / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract satisfaction
@@ Property / cites work: Abstract satisfaction / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q5457277
@@ Property / cites work: Q5457277 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q4778705
@@ Property / cites work: Q4778705 / rank @@
+Normal rank
@@ Property / cites work @@
+Program analysis via satisfiability modulo path programs
+Normal rank
@@ Property / cites work @@
+Formal verification of square root algorithms
@@ Property / cites work: Formal verification of square root algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Cutting to the Chase Solving Linear Integer Arithmetic
+Normal rank
@@ Property / cites work @@
+Solving Non-linear Arithmetic
@@ Property / cites work: Solving Non-linear Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754053
@@ Property / cites work: Q2754053 / rank @@
+Normal rank
@@ Property / cites work @@
+Generalizing DPLL to Richer Logics
@@ Property / cites work: Generalizing DPLL to Richer Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Floating-point arithmetic in the Coq system
@@ Property / cites work: Floating-point arithmetic in the Coq system / rank @@
+Normal rank
@@ Property / cites work @@
+Q4475657
@@ Property / cites work: Q4475657 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
+Normal rank
@@ Property / cites work @@
+Handbook of Floating-Point Arithmetic
@@ Property / cites work: Handbook of Floating-Point Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7<sup>™</sup> Processor
+Normal rank
@@ Property / cites work @@
+Q4904223
@@ Property / cites work: Q4904223 / rank @@
+Normal rank
@@ Property / cites work @@
+GRASP: a search algorithm for propositional satisfiability
+Normal rank
@@ Property / DOI @@
+.1007/S10703-013-0203-7
@@ Property / DOI: 10.1007/S10703-013-0203-7 / rank @@
+Normal rank