Mon 8 Jan 2018 14:00 - 14:30 at Crocker - Session 1-2 Chair(s): Kenichi Asai

Loop fusion—a program transformation to merge multiple consecutive loops into a single one—has been studied mainly for compiler optimization. In this paper, we argue that loop fusion can be useful also for program verification because it can simplify loop invariants and we propose a new loop fusion strategy, which can fuse any loops—even loops with data dependence—and preserves partial correctness.

The crux of our loop fusion is the following observation: if the state after the first loop were known, two loop bodies could be computed at the same time without suffering from data dependence by renaming program variables. Our loop fusion produces a program that guesses the unknown state after the first loop nondeterministically, executes the fused loop where variables are renamed, compares the guessed state and the state actually computed by the fused loop, and, if they do not match, diverges. The last two steps of comparison and divergence are crucial to preserve partial correctness. We call our approach ``guess-and-assume'' because, in addition to the first step to guess, the last two steps can be expressed by the pseudo-instruction assume, used in program verification.

We formalize our loop fusion for a simple imperative language and prove that it preserves partial correctness. We further extend the ``guess-and-assume'' technique to reversing loop execution, which is useful to verify a certain type of consecutive loops. Finally, we confirm by experiments that our transformation techniques can significantly reduce verification time in many cases.

Mon 8 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

14:00 - 15:30: PEPM 2018 - Session 1-2 at Crocker
Chair(s): Kenichi AsaiOchanomizu University
PEPM-201814:00 - 14:30
Akifumi ImanishiKyoto University, Kohei SuenagaGraduate School of Informatics, Kyoto University, Atsushi IgarashiKyoto University, Japan
PEPM-201814:30 - 15:00
David BromanKTH Royal Institute of Technology, Jeremy G. SiekIndiana University, USA
PEPM-201815:00 - 15:30
Ben GreenmanNortheastern University, Zeina MigeedUniversity of California, Los Angeles