Invertibility conditions for floating-point formulas
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 11599
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-030-25543-5_8
- Title of conference / published proceedings
- Computer Aided Verification
- First page
- 116
- Volume
- 11562
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- July
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
5
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Much of modern formal verification makes use of Satisfiability Modulo Theories (SMT) solvers, which can test for satisfiability of formulas making use of operators that occur commonly in programs. Two major stumbling blocks in SMT solving are floating-point numbers and universal quantification. This paper proposes a new approach to solving quantifed floating-point formulas, based on simplification routines for basic formulas called invertibility conditions. Our method has been integrated into a state-of-the-art SMT tool, CVC4.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -