Синтаксис и операционная семантика целевого языка в реализации технологии «предположи и допусти» при объединении циклов для верификации программ
Работая с нашим сайтом, вы даете свое согласие на использование файлов cookie. Это необходимо для нормального функционирования сайта, показа целевой рекламы и анализа трафика. Статистика использования сайта отправляется в «Яндекс» и «Google»
Научный журнал Моделирование, оптимизация и информационные технологииThe scientific journal Modeling, Optimization and Information Technology
Online media
issn 2310-6018

The syntax and operational semantics of the target language in the implementing the «assume and allow» technology when combining loops for program verification

Lysov D.V.  

UDC 004.7
DOI: 10.26102/2310-6018/2020.29.1.005

  • Abstract
  • List of references
  • About authors

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

Keywords: cycle transformation, program verification, cycle invariants, operational semantics, target language

For citation: Lysov D.V. The syntax and operational semantics of the target language in the implementing the «assume and allow» technology when combining loops for program verification. Modeling, Optimization and Information Technology. 2020;8(2). Available from: https://moit.vivt.ru/wp-content/uploads/2020/05/Lysov_2_20_1.pdf DOI: 10.26102/2310-6018/2020.29.1.005 (In Russ).

524

Full text in PDF