SAS 2020
Wed 18 - Fri 20 November 2020 Online Conference
co-located with SPLASH 2020
Fri 20 Nov 2020 03:00 - 03:20 at SPLASH-III - 9 Chair(s): Jerome Feret
Thu 19 Nov 2020 15:00 - 15:20 at SPLASH-III - 9 Chair(s): Kwangkeun Yi

We present an automated procedure for synthesizing sound inductive invariants for floating-point numerical loops. Our procedure generates invariants of the form of a convex polynomial inequality that tightly bounds the values of loop variables. Such invariants are a prerequisite for reasoning about the safety and roundoff errors of floating-point programs.

Unlike previous approaches that rely on policy iteration, linear algebra or semi-definite programming, we propose a heuristic procedure based on simulation and counterexample-guided refinement. We observe that this combination is remarkably effective and general and can handle both linear and nonlinear loop bodies, nondeterministic values as well as conditional statements. Our evaluation shows that our approach can efficiently synthesize loop invariants for existing benchmarks from literature, but that it is also able to find invariants for nonlinear loops that today’s tools cannot handle.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

15:00 - 16:20: 9SAS at SPLASH-III +12h
Chair(s): Kwangkeun YiSeoul National University, South Korea
15:00 - 15:20
Research paper
SAS
Anastasiia IzychevaTechnical University of Munich, Eva DarulovaMPI-SWS, Helmut SeidlTechnische Universität München
Pre-print Media Attached
15:40 - 16:00
Research paper
SAS
Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Ryota Suzuki, Takeshi TsukadaChiba University, Japan
File Attached

Fri 20 Nov
Times are displayed in time zone: Central Time (US & Canada) change

03:00 - 04:20: 9SAS at SPLASH-III
Chair(s): Jerome FeretINRIA Paris
03:00 - 03:20
Research paper
SAS
Anastasiia IzychevaTechnical University of Munich, Eva DarulovaMPI-SWS, Helmut SeidlTechnische Universität München
Pre-print Media Attached
03:40 - 04:00
Research paper
SAS
Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Ryota Suzuki, Takeshi TsukadaChiba University, Japan
File Attached