Foundations for Decision Problems in Separation Logic with General Inductive Predicates

Antonopoulos T.; Gorogiannis N.; Haase C.; M. Kanovich; Ouaknine J.

Публикации

?

Foundations for Decision Problems in Separation Logic with General Inductive Predicates

Ch. 27. P. 411–425.

Antonopoulos T., Gorogiannis N., Haase C., Канович М. И., Ouaknine J.

Язык: английский

Полный текст

Текст на другом сайте

Ключевые слова: algorithmic complexity separation logic Computer Science Applications general inductive predicates program verification

В книге

Lecture Notes in Computer Science. 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings

Berlin: Springer, 2014.

Complexity of reasoning in Kleene algebra with sum-of-letters hypotheses

Stepan L. Kuznetsov, , in: Automated Reasoning: 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part II. (LNCS, volume 16689)Vol. 16689.: Cham: Springer, 2026. P. 161–177.

Добавлено: 26 июля 2026 г.

Влияние аксиомы связности на сложность модальной логики.

Кудинов А. В., Мясников К. М., Математика и теоретические компьютерные науки 2025 Т. 3 № 2 С. 58–84

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

Добавлено: 14 октября 2025 г.

Are prime numbers and quadratic residues random?

Бланк М. Л., Discrete and Continuous Dynamical Systems 2025 Vol. 45 No. 11 P. 4186–4201

Appeals to randomness in various number-theoretic constructions appear regularly in modern scientific publications. Such famous names as V.I. Arnold, M. Katz, Ya.G. Sinai, and T. Tao are just a few examples. Unfortunately, all of these approaches rely on various, although often very non-trivial and elegant, heuristics. A new analytical approach is proposed to address the ...

Добавлено: 23 мая 2025 г.

Modification and Optimization of Pollards's Factorization ρ-Method by Means of Recursive Algorithm of Number Calculation Factorization

Смирнов И. А., Разумов П. В., Болдырихин Н. В. и др., IEEE, 2019.

Добавлено: 10 мая 2023 г.

Реализация ρ–метода факторизации Джона Полларда на языке C++

Черкесова Л. В., Сафарьян О. А., Смирнов И. А., Молодой исследователь Дона 2018 Т. 3 (12) С. 111–121

Представлен проект реализации ρ-метода факторизации Полларда на языке C++, который работает быстрее стандартного алгоритма на 27%. Это помогает значительно облегчить работу в расшифровывании и криптоанализе в различных шифрах, например, таких как RSA. ...

Добавлено: 9 мая 2023 г.

Commutative action logic

Stepan L. Kuznetsov, Journal of Logic and Computation 2023 Vol. 33 No. 6 P. 1437–1462

Добавлено: 7 марта 2023 г.

The complexity of election problems with group-separable preferences

Faliszewski P., Карпов А. В., Obraztsova S., Autonomous Agents and Multi-Agent Systems 2022 Vol. 36 Article 18

Добавлено: 14 марта 2022 г.

Mathematical Structures in Computer Science

Канович М. И., Кузнецов С. Л., Щедров А. и др., Cambridge University Press, 2019.

Добавлено: 5 февраля 2021 г.

A \(\Pi^0_1\)-bounded fragment of infinitary action logic with exponential

Кузнецов С. Л., , in: Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th BirthdayIssue 12300.: Cham: Springer, 2020. P. 3–16.

Добавлено: 25 ноября 2020 г.

23rd Conference of Open Innovations Association FRUCT, FRUCT 2018

IEEE Computer Society, 2018.

Добавлено: 1 ноября 2020 г.

14th International Scientific-Technical Conference on Actual Problems of Electronic Instrument Engineering, APEIE 2018

Novosibirsk: IEEE, 2018.

Добавлено: 23 апреля 2019 г.

On the Complexity of Pointer Arithmetic in Separation Logic.

Brotherston J., Канович М. И., , in: Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. Lecture Notes in Computer Science 11275, Springer 2018, ISBN 978-3-030-02767-4.: Netherlands: Springer, 2018. P. 329–349.

Добавлено: 5 декабря 2018 г.

Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings. Lecture Notes in Computer Science 11275, Springer 2018, ISBN 978-3-030-02767-4

Netherlands: Springer, 2018.

Добавлено: 5 декабря 2018 г.

Proceedings of 2017 VI-th International Conference on Engineering and Telecommunication (EnT) 29-30 Nov. 2017

IEEE Computer Society, 2017.

Добавлено: 4 октября 2018 г.

The Nonnegative Rank of a Matrix: Hard Problems, Easy Solutions

Шитов Я. Н., SIAM Review 2017 Vol. 59 No. 4 P. 794–800

Добавлено: 9 ноября 2017 г.

Horn fragments of the Halpern-Shoham interval temporal logic

Захарьящев М. В., BRESOLIN D., KURUCZ A. и др., , in: ACM Transactions on Computational Logic (TOCL)Vol. 18. Issue 3.: NY: ACM, 2017. P. 1–39.

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of ...

Добавлено: 17 сентября 2017 г.

Biabduction (and Related Problems) in Array Separation Logic

Канович М. И., Brotherston J., Gorogiannis N., , in: 26th International Conference on Automated Deduction – CADE 26.: Springer, 2017. P. 472–490.

Добавлено: 14 сентября 2017 г.

Model checking for symbolic-heap separation logic with inductive predicates

Brotherston J., Gorogiannis N., Kanovich Max и др., , in: POPL 2016 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.: NY: ACM, 2016. P. 84–96.

We investigate the *model checking* problem for symbolic-heap separation logic with user-defined inductive predicates, i.e., the problem of checking that a given stack-heap memory state satisfies a given formula in this language, as arises e.g. in software testing or runtime verification. First, we show that the problem is *decidable*; specifically, we present a bottom-up fixed ...

Добавлено: 9 июня 2016 г.

Two-sided unification is NP-complete

Захаров В. А., Новикова Т. А., , in: Proceedings of the 28th International Workshop on Unification, UNIF 2014. Technical report no. 14-06 in RISC Report Series.: Linz: Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, 2014. P. 55–61.

Добавлено: 13 октября 2015 г.

The Current State of Art in Program Obfuscations: Definitions of Obfuscation Security

Zakharov V.A., Kuzurin N. N., Varnovsky N. P. и др., Programming and Computer Software 2015 Vol. 41 No. 6 P. 361–372

Program obfuscation is a semantic-preserving transformation aimed at bringing a program into a form that impedes understanding of its algorithm and data structures or prevents extracting certain valuable information from the text of the program. Since obfuscation may find wide use in computer security, information hiding and cryptography, security requirements to program obfuscators have become ...

Добавлено: 13 октября 2015 г.

Комбинированное средство верификации распределённых вычислительных систем реального времени

Захаров В. А., Волканов Д. Ю., Зорин Д. А. и др., Программирование 2015 № 6 С. 72–86

Проверка правильности функционирования распределенных программ --- это одна из наиболее трудных и актуальных задач современного программирования. В статье описано комбинированное программно-инструментальное средство верификации распределенных вычислительных систем реального времени (РВС РВ). Для описания РВС РВ используется универсальный язык моделирования UML. Семантика диаграмм состояний UML определяется на основе модели вычислений иерархических временных автоматов. Средство верификации диаграмм UML ...

Добавлено: 13 октября 2015 г.

An invariant-based approach to the verification of asynchronous parameterized networks

Захаров В. А., Коннов И. В., Journal of symbolic computation 2010 Vol. 45 No. 11 P. 1144–1162

Добавлено: 12 октября 2015 г.