Conference proceeding
Invertibility Conditions for Floating-Point Formulas
Lecture Notes in Computer Science, Vol.11562, pp.116-136
07/12/2019
DOI: 10.1007/978-3-030-25543-5_8
Abstract
Automated reasoning procedures are essential for a number of applications that involve bit-exact floating-point computations. This paper presents conditions that characterize when a variable in a floating-point constraint has a solution, which we call invertibility conditions. We describe a novel workflow that combines human interaction and a syntax-guided synthesis (SyGuS) solver that was used for discovering these conditions. We verify our conditions for several floating-point formats. One implication of this result is that a fragment of floating-point arithmetic admits compact quantifier elimination. We implement our invertibility conditions in a prototype extension of our solver CVC4, showing their usefulness for solving quantified constraints over floating-points.
Details
- Title: Subtitle
- Invertibility Conditions for Floating-Point Formulas
- Creators
- Martin BrainAina NiemetzMathias PreinerAndrew ReynoldsClark BarrettCesare Tinelli
- Resource Type
- Conference proceeding
- Publication Details
- Lecture Notes in Computer Science, Vol.11562, pp.116-136
- DOI
- 10.1007/978-3-030-25543-5_8
- Publisher
- Springer
- Language
- English
- Date published
- 07/12/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259423502771
Metrics
31 Record Views