On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure

DOI10.1007/978-3-642-02658-4_42MaRDI QIDQ3636881zbMATH OpenOpenAlexFDO

Authors David Monniaux

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_42

Mathematics Subject Classification ID

Linear programming (90C05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Deciding floating-point logic with abstract conflict driven clause learning
• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
• An approximation framework for solvers and decision procedures
• Exact solutions to linear programming problems

Cited in

(10)

• SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
• Invertibility conditions for floating-point formulas
• Reluplex: a calculus for reasoning about deep neural networks
• A survey of satisfiability modulo theory
• Exploring approximations for floating-point arithmetic using UppSAT
• scientific article; zbMATH DE number 1863384 (Why is no real title available?)
• LNS with Co-Transformation Competes with Floating-Point
• An approximation framework for solvers and decision procedures
• Deferring Dag Construction by Storing Sums of Floats Speeds-Up Exact Decision Computations Based on Expression Dags
• A three-tier strategy for reasoning about floating-point numbers in SMT

Describes a project that uses

Uses Software

• MiniSat

This page was built for publication: On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure

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