ISSN 1818-1015 · EISSN 2313-5417

Язык: ru

Статья: ЛОГИКА ДЛЯ СУЖДЕНИЙ ОБ ОШИБКАХ В ЦИКЛАХ НАД ПОСЛЕДОВАТЕЛЬНОСТЯМИ ДАННЫХ (IFIL) (2023)

Читать

Читать онлайн

Классическая дедуктивная верификация не ориентирована на доказательство некорректности программ. Доказательство некорректности программ с помощью формальных методов является актуальной задачей в настоящее время. Специальные логики, такие как Incorrectness Logic, Adversarial Logic, Local Completeness Logic, Exact Separation Logic и Outcome Logic, были недавно предложены для решения данной задачи. Но у данных логик имеется два недостатка. Во-первых, в данных логиках используются подходы, основанные на нижней аппроксимации, тогда как в классической дедуктивной верификации используется подход, основанный на верхней аппроксимации. С другой стороны, использование классического подхода требует в общем случае задания инвариантов циклов. Во-вторых, использование правил вывода для программных конструкций в их самом общем виде приводит к необходимости доказательства сложных формул в простых ситуациях. Нашим результатом, представленным в данной статье, является новая логика для решения данных проблем в случае циклов над последовательностями данных. Такая циклы мы называем финитными итерациями. Предложенную логику мы называем логикой для суждений о некорректности финитных итераций (IFIL). Мы избегаем задания инвариантов финитных итераций с помощью символической замены в условиях корректности переменных таких циклов применениями рекурсивных функций. Наша логика основана на специальных правилах вывода для финитных итераций. Эти правила позволяют выводить формулы с применениями рекурсивных функций, соответствующих финитным итерациям. Истинность этих формул может означать наличие ошибок в финитных итерациях. Данная логика была реализована в новой версии программной системы C“=lightVer для дедуктивной верификации программ на языке C.

Ключевые фразы: ДЕДУКТИВНАЯ ВЕРИФИКАЦИЯ, ЛОГИКА ХОАРА, ЛОКАЛИЗАЦИЯ ОШИБОК, НЕКОРРЕКТНОСТЬ ПРОГРАММ, ИНВАРИАНТ ЦИКЛА, ФИНИТНАЯ ИТЕРАЦИЯ, C-LIGHTVER, ACL2, DEDUCTIVE VERIFICATION, HOARE LOGIC, BUG LOCALIZATION, PROGRAM INCORRECTNESS, LOOP INVARIANT, FINITE ITERATION

Автор (ы): Кондратьев Дмитрий Александрович

Журнал: МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ

Идентификаторы и классификаторы

УДК: 004.052.42. Обнаружение ошибок. Проверка достоверности данных. Верификация данных
eLIBRARY ID: 54489243

Для цитирования:

КОНДРАТЬЕВ Д. А. ЛОГИКА ДЛЯ СУЖДЕНИЙ ОБ ОШИБКАХ В ЦИКЛАХ НАД ПОСЛЕДОВАТЕЛЬНОСТЯМИ ДАННЫХ (IFIL) // МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ. 2023. Т. 30 № 3

Текстовый фрагмент статьи

Моя история просмотров (5)

01. Статья: ФОРМЫ ПРОЯВЛЕНИЯ ЭКОНОМИЧЕСКОЙ ПРЕСТУПНОСТИ В РОССИИ И МЕРЫ ЕЕ НИВЕЛИРОВАНИЯ

02. Статья: СТОХАСТИЧЕСКИЙ АНАЛИЗ И МОДЕЛИРОВАНИЕ ЭКСТРЕМАЛЬНЫХ ВОЛН

03. Статья: АНАЛИЗ ГРАФОВ И ВЫЯВЛЕНИЯ СЕТЕВЫХ МОТИВОВ

04. Статья: ОСОБЫЙ ПРОТИВОПОЖАРНЫЙ РЕЖИМ КАК ЭКСТРАОРДИНАРНЫЙ РЕЖИМ ДЕЯТЕЛЬНОСТИ ПУБЛИЧНОЙ АДМИНИСТРАЦИИ

05. Статья: СОСТАВЛЕНИЕ РАСПИСАНИЙ КАК ЗАДАЧА УДОВЛЕТВОРЕНИЯ ОГРАНИЧЕНИЙ (НА ПРИМЕРЕ ПЛАНИРОВАНИЯ ОТКРЫТЫХ ГОРНЫХ РАБОТ)

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

R. H“ahnle and M. Huisman, “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools”, in Computing and Software Science, vol. 10000, Springer, 2019, pp. 345-373.
K. R. Apt and E.-R. Olderog, “Fifty years of Hoare’s logic”, Formal Aspects of Computing, vol. 31, no. 6, pp. 751-807, 2019. EDN: UKBEZU
K. R. Apt and E.-R. Olderog, “Assessing the Success and Impact of Hoare’s Logic”, in Theories of Programming: The Life and Works of Tony Hoare, 2021, pp. 41-76.
C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM, vol. 12, no. 10, pp. 576-580, 1969.
B. M“oller, P. O’Hearn, and T. Hoare, “On Algebra of Program Correctness and Incorrectness”, in Relational and Algebraic Methods in Computer Science, vol. 13027, Springer, 2021, pp. 325-343.
Q. L. Le, A. Raad, J. Villard, J. Berdine, D. Dreyer, and P. W. O’Hearn, “Finding Real Bugs in Big Programs with Incorrectness Logic”, Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA1, pp. 1-27, 2022.
P. W. O’Hearn, “Incorrectness logic”, Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 1-32, 2019.
A. Raad, J. Berdine, H.-H. Dang, D. Dreyer, P. O’Hearn, and J. Villard, “Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic”, in Computer Aided Verification, vol. 12225, Springer, 2020, pp. 225-252.
J. Vanegue, “Adversarial Logic”, in Static Analysis, vol. 13790, Springer, 2022, pp. 422-448.

M. Milanese and F. Ranzato, "Local Completeness Logic on Kleene Algebra with Tests", in Static Analysis, vol. 13790, Springer, 2022, pp. 350-371.

B. Bruni, R. Giacobazzi, R. Gori, and F. Ranzato, "A Correctness and Incorrectness Program Logic", Journal of the ACM, vol. 70, no. 2, pp. 1-45, 2023.

P. Maksimovi\'c, C. Cronj"ager, A. L"o"ow, J. Sutherland, and P. Gardner, "Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding", in 37th European Conference on Object-Oriented Programming (ECOOP 2023), vol. 263, Schloss Dagstuhl - Leibniz-Zentrum f"ur Informatik, 2023, pp. 19:1-19:27.

N. Zilberstein, D. Dreyer, and A. Silva, "Outcome Logic: A Unifying Foundation of Correctness and Incorrectness Reasoning", Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 522-550, 2023.

T. Dardinier and P. M"uller, "Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)". 2023.

A. Humenberger, M. Jaroschek, and L. Kov\'acs, "Invariant Generation for Multi-Path Loops with Polynomial Assignments", in Verification, Model Checking, and Abstract Interpretation, vol. 10747, Springer, 2018, pp. 226-246.

S. Chakraborty, A. Gupta, and D. Unadkat, "Full-program induction: verifying array programs sans loop invariants", International Journal on Software Tools for Technology Transfer, vol. 24, no. 5, pp. 843-888, 2022.  EDN: WCALXU

V. A. Nepomniaschy, "Symbolic method of verification of definite iterations over altered data structures", Programming and Computer Software, vol. 31, no. 1, pp. 1-9, 2005.  EDN: HSBRRT

V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhailov, and A. V. Promskii, "Towards verification of C programs. C-light language and its formal semantics", Programming and Computer Software, vol. 28, no. 6, pp. 314-323, 2002.  EDN: LHCEKP

V. A. Nepomniaschy, I. S. Anureev, and A. V. Promskii, "Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language", Programming and Computer Software, vol. 29, no. 6, pp. 338-350, 2003.  EDN: LHWXPB

I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, and D. A. Kondratyev, "Automatic C Program Verification Based on Mixed Axiomatic Semantics", Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 407-414, 2014.  EDN: UOLVCP

D. A. Kondratyev and V. A. Nepomniaschy, "Automation of C Program Deductive Verification without Using Loop Invariants", Programming and Computer Software, vol. 48, no. 5, pp. 331-346, 2022.  EDN: MIMTLQ

D. A. Kondratyev and A. V. Promsky, "The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs", Automatic Control and Computer Sciences, vol. 54, no. 7, pp. 728-739, 2020.  EDN: OQPQSY

J. S. Moore, "Milestones from the Pure Lisp Theorem Prover to ACL2", Formal Aspects of Computing, vol. 31, no. 6, pp. 699-732, 2019.

D. A. Kondratyev, I. V. Maryasov, and V. A. Nepomniaschy, "The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination", Automatic Control and Computer Sciences, vol. 53, no. 7, pp. 653-662, 2019.  EDN: ALYSLL

L. Zhang and B. L. Kaminski, "Quantitative strongest post: a calculus for reasoning about the flow of quantitative information", Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA1, pp. 1-29, 2022.

S. Dailler, D. Hauzar, C. March\'e, and Y. Moy, "Instrumenting a weakest precondition calculus for counterexample generation", Journal of Logical and Algebraic Methods in Programming, vol. 99, pp. 97-113, 2018.

B. Becker, C. B. Louren\cco, and C. March\'e, "Explaining Counterexamples with Giant-Step Assertion Checking", in Proceedings of the 6th Workshop on Formal Integrated Development Environment, vol. 338, 2021, pp. 82-88.

Q. L. Le, J. Sun, L. H. Pham, and S. Qin, "S2TD: a Separation Logic Verifier that Supports Reasoning of the Absence and Presence of Bugs". 2022.

T. Dardinier, G. Parthasarathy, and P. M"uller, "Verification-Preserving Inlining in Automatic Separation Logic Verifiers", Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 789-818, 2023.

R. K"onighofer, R. Toegl, and R. Bloem, "Automatic Error Localization for Software Using Deductive Verification", in Hardware and Software: Verification and Testing, vol. 8855, Springer, 2014, pp. 92-98.

P. Baudin et al., "The dogged pursuit of bug-free C programs: the Frama-C software analysis platform", Communications of the ACM, vol. 64, no. 8, pp. 56-68, 2021.  EDN: SQNOYR

M. R. Gadelha, F. Monteiro, L. Cordeiro, and D. Nicole, "ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference", in Tools and Algorithms for the Construction and Analysis of Systems, vol. 11429, Springer, 2019, pp. 209-213.

S. L"owe, "CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation", in Tools and Algorithms for the Construction and Analysis of Systems, vol. 7795, Springer, 2013, pp. 610-612.

D. Beyer and T. Lemberger, "CPA-SymExec: efficient symbolic execution in CPAchecker", in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 900-903.

C. Cadar and M. Nowack, "KLEE symbolic execution engine in 2019", International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 867-870, 2021.  EDN: JIAYUP

B. Jacobs, J. Kiniry, and M. Warnier, "Java Program Verification Challenges", in Formal Methods for Components and Objects, vol. 2852, Springer, 2003, pp. 202-219.

Выпуск

Т. 30 № 3 (2023)

Кол-во страниц: 90 страниц

Другие статьи выпуска

АЛГОРИТМЫ ДЛЯ ЗАДАЧ ОБ ЭЙЛЕРОВОМ ЦИКЛЕ И ЭЙЛЕРОВОЙ ЦЕПИ В КРАТНОМ ГРАФЕ (2023)

Авторы: Смирнов Александр Валерьевич

В статье рассматриваются неориентированные кратные графы произвольной натуральной кратности k>1. Кратный граф содержит ребра трех типов: обычные, кратные и мультиребра. Ребра последних двух типов представляют собой объединение k связанных ребер, которые соединяют 2 или (k+1) вершину соответственно. Связанные ребра могут использоваться только согласованно. Если вершина инцидентна кратному ребру, то она может быть инцидентна другим кратным ребрам, а также она может быть общим концом k связанных ребер мультиребра. Если вершина является общим концом мультиребра, то она не может быть общим концом никакого другого мультиребра. Ставится задача об эйлеровом маршруте (цикле или цепи) в кратном графе, которая обобщает классическую задачу для обычного графа. Сформулированы необходимые условия существования эйлерова маршрута в кратном графе, показано, что эти условия не являются достаточными. Кроме того, показано, что для произвольного кратного графа необходимые условия существования эйлерова цикла и эйлеровой цепи не являются взаимоисключающими, поэтому можно построить кратный граф, в котором одновременно существуют два вида эйлеровых маршрутов. Кратному графу сопоставляется обычный граф с квазивершинами, в упрощенном виде представляющий структуру исходного графа. В частности, каждому эйлерову маршруту в кратном графе соответствует эйлеров маршрут в графе с квазивершинами. Формулируется алгоритм построения такого графа. Также рассмотрена вспомогательная задача о покрывающих цепях с заданными концами в обычном графе, получены два алгоритма ее решения. Разработан алгоритм поиска эйлерова маршрута в кратном графе экспоненциальной трудоемкости. Для частного случая кратного графа предложен полиномиальный алгоритм, показано, что в этом частном случае необходимые условия существования эйлерова маршрута являются достаточными.

Сохранить в закладках

ПРИМЕНЕНИЕ АЛГОРИТМА ПОИСКА ВНЕШНЕЙ МЕДИАНЫ ГРАФА В ЗАДАЧАХ ОПРЕДЕЛЕНИЯ НАДЕЖНОСТИ ТЕХНИЧЕСКИХ СИСТЕМ (2023)

Авторы: Тихонов Владимир Борисович, Плакса Юрий Андреевич, Курочкина Светлана Алексеевна, Прусова Наталия Александровна

Рассмотрена задача о размещении центра обслуживания технических систем при известных значениях потоков отказов. Даная задача решалась с помощью минисуммного алгоритма теории графов. Получена зависимость коэффициента готовности системы от среднего времени наработки между отказами и среднего времени восстановления элементов системы. Показано, что оптимальным местом расположения пункта технического обслуживания является медиана графа, расположенная в одной из его вершин.

Сохранить в закладках

РАСПРЕДЕЛЕНИЕ БОЛЬЦМАНА В ПРОБЛЕМЕ РАЦИОНАЛЬНОГО ВЫБОРА ПОПУЛЯЦИЕЙ УЧАСТКА ПРИ НЕПОЛНОЙ ИНФОРМАЦИИ О ЕГО РЕСУРСАХ (2023)

Авторы: Кириллов Александр Николаевич, Данилова Инна Владимировна

Рассматривается задача рационального выбора популяцией участка, содержащего энергетические (пищевые) ресурсы. Рассматриваемая задача относится к теории оптимального фуражирования, которая в свою очередь изучает вопросы, касающиеся поведения популяции, когда она покидает участок или выбирает наиболее подходящий. Для определения оптимального для популяции выбора участка предлагается вариационный подход, основанный на идее распределения Больцмана. Для построения распределения Больцмана вводятся функции полезности, которые учитывают факторы, способные повлиять на выбор популяции: имеющаяся информация о качестве участков, энергетическая полезность участков, затраты на перемещение к участку, стоимость информации о качестве участков. Основная цель статьи - исследовать влияние имеющейся информации о количестве ресурсов, содержащихся в участках, на процесс принятия решений, генерируемых популяцией при выборе подходящего участка. Оптимальная рациональность определяется с учетом стоимости информации, средней энергетической ценности всех участков, рациональности, зависящей от качества участка. Получены условия, при которых популяция при недостатке информации выбирает «бедный» участок в смысле энергетической ценности (ресурсов). Последнее дает теоретическое обоснование экспериментальным наблюдениям, согласно которым, популяция может выбрать участок худшего качества. Полученные результаты носят общий характер и могут быть использованы не только в поведенческой экологии, но и при построении любых процессов принятия решений.

Сохранить в закладках

КЛАССИФИКАЦИЯ ТЕКСТОВ ПО УРОВНЯМ CEFR С ИСПОЛЬЗОВАНИЕМ МЕТОДОВ МАШИННОГО ОБУЧЕНИЯ И ЯЗЫКОВОЙ МОДЕЛИ BERT (2023)

Авторы: Лагутина Надежда Станиславовна, Касаткина Наталья Николаевна, Лагутина Ксения Владимировна, Бредерман А. М.

В данной работе представлено исследование задачи автоматической классификации коротких связных текстов (эссе) на английском языке по уровням международной шкалы CEFR. Определение уровня текста на естественном языке является важной составляющей оценки знаний учащихся, в том числе для проверки открытых заданий в системах электронного обучения. Для решения этой задачи были рассмотрены векторные модели текста на основе стилометрических числовых характеристик уровня символов, слов, структуры предложения. Классификация полученных векторов осуществлялась стандартными классификаторами машинного обучения. В статье приведены результаты трёх наиболее успешных: Support Vector Classifier, Stochastic Gradient Descent Classifier, LogisticRegression. Оценкой качества послужили точность, полнота и F“=мера. Для экспериментов были выбраны два открытых корпуса текстов CEFR Levelled English Texts и BEA“=2019. Лучшие результаты классификации по шести уровням и подуровням CEFR от A1 до C2 показал Support Vector Classifier с F“=мерой 67 % для корпуса CEFR Levelled English Texts. Этот подход сравнивался с применением языковой модели BERT (шесть различных вариантов). Лучшая модель bert“=base“=cased обеспечила значение F“=меры 69 %. Анализ ошибок классификации показал, что большая их часть допущена между соседними уровнями, что вполне объяснимо с точки зрения предметной области. Кроме того, качество классификации сильно зависело от корпуса текстов, что продемонстрировало существенное различие F“=меры в ходе применения одинаковых моделей текста для разных корпусов. В целом, полученные результаты показали эффективность автоматического определения уровня текста и возможность его практического применения.

Сохранить в закладках

ОБОБЩЕННЫЕ ТИПИЗИРОВАННЫЕ ЗАВИСИМОСТИ ВКЛЮЧЕНИЯ С НЕОПРЕДЕЛЕННЫМИ ЗНАЧЕНИЯМИ В БАЗАХ ДАННЫХ (2023)

Авторы: Зыкин Сергей Владимирович

В статье рассматривается новый вид зависимостей в базах данных, являющийся обобщением зависимостей включения. Традиционно такие зависимости на практике используются для обеспечения ссылочной целостности. При этом, ограничение устанавливается только между парой отношений, первое из которых называется главным, второе - внешним. На практике ссылочную целостность часто требуется установить для большего числа отношений, где в одном ограничении участвуют несколько главных и несколько подчиненных отношений. Такая структура соответствует ультраграфу. В работе приведено обоснование обобщенных зависимостей включения, учитывающих наличие неопределенных значений во внешних отношениях. На основе исследования свойств типизированных зависимостей получена система аксиом, для которой доказана непротиворечивость (надежность) и полнота.

Сохранить в закладках

Издательство

Издательство: ЯрГУ им. П.Г. Демидова
Регион: Россия, Ярославль
Почтовый адрес: 150003, Ярославль, Советская, 14,
Юр. адрес: 150003, Ярославль, Советская, 14,
ФИО: Иванчин Артем Владимирович (Ректор)
E-mail адрес: rectorat@uniyar.ac.ru
Контактный телефон: +7 (485) 2797702
Сайт: https://www.uniyar.ac.ru/

Все права на тексты и товарные знаки принадлежат их законным владельцам. Подробнее...

Сайт https://scinetwork.ru (далее – сайт) работает по принципу агрегатора – собирает и структурирует информацию из публичных источников в сети Интернет, то есть передает полнотекстовую информацию о товарных знаках в том виде, в котором она содержится в открытом доступе.

Сайт и администрация сайта не используют отображаемые на сайте товарные знаки в коммерческих и рекламных целях, не декларируют своего участия в процессе их государственной регистрации, не заявляют о своих исключительных правах на товарные знаки, а также не гарантируют точность, полноту и достоверность информации.

Все права на товарные знаки принадлежат их законным владельцам!

Сайт носит исключительно информационный характер, и предоставляемые им сведения являются открытыми публичными данными.

Администрация сайта не несет ответственность за какие бы то ни было убытки, возникающие в результате доступа и использования сайта.

Спасибо, понятно.