Deciding floating-point logic with abstract conflict driven clause learning

DOI10.1007/S10703-013-0203-7zbMath1317.68110OpenAlexW2127145687WikidataQ59395541 ScholiaQ59395541MaRDI QIDQ479837

Vijay D'Silva, Daniel Kroening, Martin Brain, Alberto Griggio, Leopold Haller

Publication date: 5 December 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-013-0203-7

zbMATH Keywords

abstract interpretationSMTdecision proceduresfloating-point logic

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (14)

Abstract interpretation as automated deduction ⋮ An approximation framework for solvers and decision procedures ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Abstract Interpretation as Automated Deduction ⋮ Correct approximation of IEEE 754 floating-point arithmetic for program verification ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ raSAT: an SMT solver for polynomial constraints ⋮ A two-phase approach for conditional floating-point verification ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Optimization modulo the theory of floating-point numbers ⋮ A Survey of Satisfiability Modulo Theory ⋮ An SMT theory of fixed-point arithmetic

Uses Software

• Unnamed Item
• z3
• HOL Light
• MathSAT5
• CBMC
• ASTREE
• SONOLAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Floating-point arithmetic in the Coq system
• Formal verification of square root algorithms
• Generalizing DPLL and satisfiability for equalities
• Numeric Bounds Analysis with Conflict-Driven Learning
• Solving Non-linear Arithmetic
• An Abstract Interpretation of DPLL(T)
• Abstract conflict driven learning
• The Reduced Product of Abstract Domains and the Combination of Decision Procedures
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• Natural Domain SMT: A Preliminary Assessment
• Handbook of Floating-Point Arithmetic
• Generalizing DPLL to Richer Logics
• An Abstract Domain to Discover Interval Linear Equalities
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• GRASP: a search algorithm for propositional satisfiability
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables
• Cutting to the Chase Solving Linear Integer Arithmetic
• Program analysis via satisfiability modulo path programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Programming Languages and Systems
• Programming Languages and Systems
• Computer Aided Verification
• The MathSAT5 SMT Solver
• Splitting on Demand in SAT Modulo Theories
• Abstract satisfaction
• A machine program for theorem-proving
• Computer Aided Verification
• Multi-Prover Verification of Floating-Point Programs

This page was built for publication: Deciding floating-point logic with abstract conflict driven clause learning