Loop Fusion – Converting a program to combine multiple consecutive loops into one – has
been studied mainly for compiler optimization. The paper proposes a new strategy for combining loops,
which can combine any loops even loops with data dependency. It is shown that this is useful for the
verification program, because it can simplify cycle invariants. The essence of the merge cycle is as
follows: if the state after the first cycle was known, two bodies of the cycle can be calculated
simultaneously, regardless of the data by renaming the program variables. Loop Fusion creates a
program that guesses an unknown state after the first cycle, non-deterministically executes a merged
cycle in which variables are renamed, compares the guessed state and the state actually calculated by
the merged loop, and, if they do not match, diverges. The last two steps of the comparison and the discrepancy are crucial for maintaining partial correctness. The «suppose and allow» approach is so
named because, in addition to the first step (suppose), the last two steps can be expressed by the «allow»
pseudo-instruction used in program verification.
1. Bacon D.F., Graham S.L., Sharp O.J. Compiler Transformations for High-performance
Computing. ACM Comput. Surv. 1994;26(4):345-420.
2. Beyer D., Keremoglu M.E. CPAchecker: A Tool for Configurable Software Verification.
CAV 2011 (LNCS). Springer. 2011;6806:184-190.
3. Cohen E. Information transmission in computational systems. ACM SIGOPS Operating
Systems Review. ACM. 1977;11:133-139
4. Ferrante J., Ottenstein K.J., Warren J.D. The Program Dependence Graph and Its Use in
Optimization. ACM Trans. Program. Lang. Syst. 1987;9(3):319-349
5. Goguen J.A., Meseguer J. Security Policies and Security Models. 1982 IEEE Symposium
on Security and Privacy, Oakland, CA, USA. 1982:11-20.
6. Gurfinkel A., Kahsai T., Komuravelli A., Navas J.A. The SeaHorn verification framework.
CAV 2015 (LNCS), Vol. 9206. Springer. 2015:343-361.
7. Li P., Zdancewic S. Downgrading policies and relaxed noninterference. Proc. of the 32nd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2005, Long Beach, California, USA. 2005:158-170.
8. McLean J. Security Models and Information Flow. Proc. of the IEEE Symposium on
Security and Privacy, Oakland, California, USA. 1990:180-189.
9. Terauchi T., Aiken A. Secure Information Flow as a Safety Problem. Static Analysis, 12th
Int. Symposium, SAS 2005, London, UK. 2005:352-367.
10. Winskel G. The Formal Semantics of Programming Languages: An Introduction. The MIT
Press. 1993.
11. Barnett M., Chang B.-Y.E., DeLine R., Jacobs B., Leino K.R.M. Boogie: A Modular
Reusable Verifier for Object-Oriented Programs. FMCO 2005 (LNCS). 2005;4111:364-
387.
12. Reynolds J.C. Separation Logic: A Logic for Shared Mutable Data Structures. Proc. of
IEEE Symposium on Logic In Computer Science (LICS’02). 2002.
Lysov Dmitry Vyacheslavovich
Email: csit@bk.ru
Voronezh State Technical University
Voronezh, Russian Federation
