Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов


https://doi.org/10.18255/1818-1015-2018-5-491-505

Полный текст:


Аннотация

При дедуктивной верификации программ, написанных на императивных языках программирования, особую сложность вызывает порождение и доказательство условий корректности, соответствующих циклам, поскольку каждый из них должен быть снабжён инвариантом, построение которого часто является нетривиальной задачей. Методы синтеза инвариантов циклов, как правило, носят эвристический характер, что затрудняет их применение. Альтернативой является символический метод элиминации инвариантов циклов, предложенный В.А. Непомнящим в 2005 году. Его идея состоит в представлении тела цикла в виде специальной операции замены при выполнении определённых ограничений. Такая операция в символической форме выражает действие цикла, что позволяет ввести в аксиоматическую семантику правило вывода для циклов, не использующее инварианты. В данной работе представлено дальнейшее развитие этого метода. Он расширяет метод смешанной аксиоматической семантики, предложенный для верификации C-light программ. Данное расширение включает в себя метод верификации итераций над изменяемыми массивами с возможным выходом из тела цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов циклов. Данное правило было реализовано в генераторе условий корректности, являющемся частью системы автоматизированной верификации C-light программ. Для проведения автоматического доказательства в используемой системе ACL2 были разработаны и реализованы два алгоритма: первый порождает операцию замены на языке системы ACL2, а второй генерирует вспомогательные леммы, позволяющие системе ACL2 успешно доказать получаемые условия корректности в автоматическом режиме. Применение вышеуказанных методов и алгоритмов проиллюстрировано примером.


Об авторах

Дмитрий Александрович Кондратьев
Институт систем информатики им. А.П. Ершова СО РАН.
Россия

аспирант.

Новосибирск.



Илья Владимирович Марьясов
Институт систем информатики им. А.П. Ершова СО РАН.
Россия

канд. физ.-мат. наук.

Новосибирск.



Валерий Александрович Непомнящий
Институт систем информатики им. А.П. Ершова СО РАН.
Россия

канд. физ.-мат. наук.

Новосибирск.



Список литературы

1. Anureev I. S., Maryasov I. V., Nepomniaschy V. A., “C-programs Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 45:7 (2011), 485–500.

2. Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S., “VCC: A Practical System for Verifying Concurrent C”, 22nd Int. Conf. TPHOLs, LNCS, 5674 (2009), 23–42.

3. Dongarra J. J., van der Steen A. J., “High-performance computing systems: Status and outlook”, Acta Numerica, 21 (2012), 379–474.

4. Filliˆatre J.-C., March´e C., “Multi-prover Verification of C Programs”, 6th ICFEM, LNCS, 3308 (2004), 15–29.

5. Jacobs B., Kiniry J. L., Warnier M., “Java Program Verification Challenges”, FMCO 2002, LNCS, 2852 (2003), 202–219.

6. Kaufmann M., Moore J.S., “An Industrial Strength Theorem Prover for a Logic Based on Common Lisp”, IEEE Transactions on Software Engineering, 23:4 (1997), 203–213.

7. Kondratyev D., “Implementing the Symbolic Method of Verification in the C-Light Project”, PSI 2017, LNCS, 10742 (2018), 227–240.

8. Kondratyev D.A., “Towards Loop Invariant Elimination for Definite Iterations over Changeable Data Structures in C Programs Verification. Appendices”, https:// bitbucket.org/c-light/loop-invariant-elimination.

9. Kondratyev D.A., Maryasov I.V., Nepomniaschy V.A., “Towards Loop Invariant Elimination for Definite Iterations over Changeable Data Structures in C Programs Verification”, PSSV 2018, Workshop Proceedings, Yaroslavl, 2018, 51–57.

10. Li J., Sun J., Li L., Loc Le Q., Lin S-W., “Automatic Loop Invariant Generation and Refinement through Selective Sampling”, 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2017, 782–792.

11. Maryasov I.V., Nepomniaschy V.A., “Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs”, Modeling and Analysis of Information Systems, 22:6 (2015), 773–782.

12. Maryasov I.V., Nepomniaschy V.A., Kondratyev D.A., “Invariant Elimination of Definite Iterations over Arrays in C Programs Verification”, Modeling and Analysis of Information Systems, 24:6 (2017), 743–754.

13. Maryasov I.V., Nepomniaschy V.A., Promsky A.V., Kondratyev D.A., “Automatic C Program Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 48:7 (2014), 407–414.

14. Nepomniaschy V.A., “Symbolic Method of Verification of Definite Iterations over Altered Data Structures”, Programming and Computer Software, 31:1 (2005), 1–9.

15. Tuerk T., “Local Reasoning about While-Loops”, VSTTE 2010, Workshop Proceedings, 2010, 29–39.


Дополнительные файлы

Для цитирования: Кондратьев Д.А., Марьясов И.В., Непомнящий В.А. Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов. Моделирование и анализ информационных систем. 2018;25(5):491-505. https://doi.org/10.18255/1818-1015-2018-5-491-505

For citation: Kondratyev D., Maryasov I., Nepomniaschy V. The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination. Modeling and Analysis of Information Systems. 2018;25(5):491-505. (In Russ.) https://doi.org/10.18255/1818-1015-2018-5-491-505

Просмотров: 196

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)