Invertibility conditions for floating-point formulas
- Submitting institution
-
City, University of London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 821
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-030-25543-5_8
- Title of conference / published proceedings
- Computer Aided Verification. CAV 2019
- First page
- 116
- Volume
- 11562 LNCS
- 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
- Quantifiers over theories and floating-point (FP) are two of the most challenging areas of Satisfiability Modulo Theories (SMT). This output creates an entirely new approach to handling them. The formally verified results and demonstrable improvements in state-of-the-art are only possible in the last years due to the work of the authors (Niemetz et al 2018; Brain et al 2019; Nötzli, et al 2019).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
