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

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

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

15:00 - 16:20
9SAS at SPLASH-III +12h
Chair(s): Kwangkeun Yi Seoul National University, South Korea
15:00
20m
Research paper
Counterexample- and Simulation-Guided Floating-Point Loop Invariant SynthesisArtifact
SAS
Anastasia Isychev Technical University of Munich, Eva Darulova MPI-SWS, Helmut Seidl Technische Universität München
Pre-print Media Attached
15:40
20m
Research paper
Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking
SAS
Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Ryota Suzuki , Takeshi Tsukada Chiba University, Japan
File Attached

Fri 20 Nov

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

03:00 - 04:20
9SAS at SPLASH-III
Chair(s): Jerome Feret INRIA Paris
03:00
20m
Research paper
Counterexample- and Simulation-Guided Floating-Point Loop Invariant SynthesisArtifact
SAS
Anastasia Isychev Technical University of Munich, Eva Darulova MPI-SWS, Helmut Seidl Technische Universität München
Pre-print Media Attached
03:40
20m
Research paper
Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking
SAS
Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Ryota Suzuki , Takeshi Tsukada Chiba University, Japan
File Attached