Invertibility conditions for floating-point formulas

DOI10.1007/978-3-030-25543-5_8MaRDI QIDQ6154876zbMATH OpenOpenAlexFDO

Authors Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Publication date 16 February 2024

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-25543-5_8

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Solving quantified bit-vectors using invertibility conditions
• On solving quantified bit-vector constraints using invertibility conditions
• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Deciding floating-point logic with abstract conflict driven clause learning
• On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure

This page was built for publication: Invertibility conditions for floating-point formulas

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