Invertibility Conditions for Floating-Point Formulas

被引：4

作者：

Brain, Martin ^{[3
,4
]}

Niemetz, Aina ^{[1
]}

Preiner, Mathias ^{[1
]}

Reynolds, Andrew ^{[2
]}

Barrett, Clark ^{[1
]}

Tinelli, Cesare ^{[2
]}

机构：

[1] Stanford Univ, Stanford, CA 94305 USA

[2] Univ Iowa, Iowa City, IA USA

[3] Univ Oxford, Oxford, England

[4] City Univ London, London, England

来源：

COMPUTER AIDED VERIFICATION, CAV 2019, PT II | 2019年 / 11562卷

基金：

美国国家科学基金会;

关键词：

D O I：

10.1007/978-3-030-25543-5_8

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：116 / 136

页数：21

共 33 条

[1] Scaling Enumerative Program Synthesis via Divide and Conquer [J].

Alur, Rajeev ;

Radhakrishna, Arjun ;

Udupa, Abhishek .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT I, 2017, 10205 :319-336

[2] Syntax-Guided Synthesis [J].

Alur, Rajeev ;

Bodik, Rastislav ;

Dallal, Eric ;

Fisman, Dana ;

Garg, Pranav ;

Juniwal, Garvit ;

Kress-Gazit, Hadas ;

Madhusudan, P. ;

Martin, Milo M. K. ;

Raghothaman, Mukund ;

Saha, Shamwaditya ;

Seshia, Sanjit A. ;

Singh, Rishabh ;

Solar-Lezama, Armando ;

Torlak, Emina ;

Udupa, Abhishek .

DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2015, 40 :1-25

[3] Automatic Detection of Floating-Point Exceptions [J].

Barr, Earl T. ;

Thanh Vo ;

Vu Le ;

Su, Zhendong .

ACM SIGPLAN NOTICES, 2013, 48 (01) :549-560

[4]

Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14

[5]

Barrett C., 2010, The satisfiability modulo theories library (SMT-LIB)

[6]

Ben Khadra MA, 2017, PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), P11, DOI 10.23919/FMCAD.2017.8102235

[7]

Bjorner N., 2015, 20 INT C LOG PROGR A, V35, P15

[8] A SIMPLE UNPREDICTABLE PSEUDORANDOM NUMBER GENERATOR [J].

BLUM, L ;

BLUM, M ;

SHUB, M .

SIAM JOURNAL ON COMPUTING, 1986, 15 (02) :364-383

[9] Building Better Bit-Blasting for Floating-Point Problems [J].

Brain, Martin ;

Schanda, Florian ;

Sun, Youcheng .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, 2019, 11427 :79-98

[10] An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic [J].

Brain, Martin ;

Tinelli, Cesare ;

Rummer, Philipp ;

Wahl, Thomas .

IEEE 22ND SYMPOSIUM ON COMPUTER ARITHMETIC ARITH 22, 2015, :160-167

← 1 2 3 4 →