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

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Session 1-2PEPM at Crocker
Chair(s): Kenichi Asai Ochanomizu University
14:00
30m
Talk
A Guess-and-Assume Approach to Loop Fusion for Program Verification
PEPM
Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University, Japan
DOI
14:30
30m
Talk
Gradually Typed Symbolic Expressions
PEPM
David Broman KTH Royal Institute of Technology, Jeremy G. Siek Indiana University, USA
DOI
15:00
30m
Talk
On the Cost of Type-Tag Soundness
PEPM
Ben Greenman Northeastern University, Zeina Migeed University of California, Los Angeles
DOI