SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Tue 19 Oct 2021 07:40 - 07:55 at Zurich D - Session 4C Chair(s): Jerome Feret
Tue 19 Oct 2021 15:40 - 15:55 at Zurich D - Session 4C Chair(s): Suvam Mukherjee

In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art techniques for precision tuning use a try and fail approach. They change the data types of some variables of the program and evaluate the accuracy of the result. Depending on what is obtained, they change more or less data types and repeat the process. Our technique is radically different. Based on semantic equations, we generate an Integer Linear Problem (ILP) from the program source code. Basically, this is done by reasoning on the most significant bit and the number of significant bits of the values which are integer quantities. The integer solution to this problem, computed in polynomial time by a classical linear programming solver, gives the optimal data types at the bit level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So we use policy iteration to find the solution. Both techniques have been implemented and we show that our results encompass the results of state-of-the-art tools.

Tue 19 Oct

Displayed time zone: Central Time (US & Canada) change

07:40 - 09:00
Session 4CSAS at Zurich D
Chair(s): Jerome Feret INRIA Paris
07:40
15m
Talk
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia
07:55
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban École normale supérieure
08:10
15m
Talk
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder
08:25
15m
Talk
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba
08:40
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS

15:40 - 17:00
Session 4CSAS at Zurich D -8h
Chair(s): Suvam Mukherjee Microsoft Research
15:40
15m
Talk
Fast and Efficient Bit-Level Precision TuningVirtual
SAS
Assalé Adjé Université de Perpignan Via Domitia, Dorra Ben Khalifa Université de Perpignan Via Domitia, Matthieu Martel Université de Perpignan Via Domitia
15:55
15m
Talk
Reduced Products of Abstract Domains for Fairness Certification of Neural NetworksVirtual
SAS
Denis Mazzucato INRIA & École Normale Supérieure, Caterina Urban École normale supérieure
16:10
15m
Talk
Static analysis of ReLU neural networks with tropical polyhedraVirtual
SAS
Eric Goubault Ecole Polytechnique, Sebastien Palumby Ecole Polytechnique, Sylvie Putot École Polytechnique, Louis Rustenholz École Polytechnique, Sriram Sankaranarayanan University of Colorado, Boulder
16:25
15m
Talk
Toward Neural-Network-Guided Program Synthesis and VerificationVirtual
SAS
Naoki Kobayashi University of Tokyo, Japan, Taro Sekiyama National Institute of Informatics, Issei Sato The University of Tokyo, Hiroshi Unno University of Tsukuba
16:40
20m
Live Q&A
Session 4C Discussion, Questions and AnswersVirtual
SAS