?
Foundations for Decision Problems in Separation Logic with General Inductive Predicates
Ch. 27. P. 411–425.
Antonopoulos T., Gorogiannis N., Haase C., Kanovich M., Ouaknine J.
We establish foundational results on the computational complexity of deciding entailment in Separation Logic with general inductive predicates whose underlying base language allows for pure formulas, pointers and existentially quantified variables. We show that entailment is in general undecidable, and ExpTime-hard in a fragment recently shown to be decidable by Iosif et al. Moreover, entailment in the base language is PI_2^p complete, the upper bound even holds in the presence of list predicates. We additionally show that entailment in essentially any fragment of Separation Logic allowing for general inductive predicates is intractable even when strong syntactic restrictions are imposed.
Kudinov A., Мясников К. М., Математика и теоретические компьютерные науки 2025 Т. 3 № 2 С. 58–84
The paper proves that for weakly transitive logics with the universal modality, whose formula satisfiability problem is in PSPACE, adding the connectedness axiom does not increase the complexity. Furthermore, an explicit algorithm solving this problem is presented. ...
Added: October 14, 2025
Blank M., 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 ...
Added: May 23, 2025
Смирнов И. А., Разумов П. В., Болдырихин Н. В. et al., IEEE, 2019.
Investigations of cryptographic algorithms for
today are very actually in connection with cybernetic attacks
threat and necessity of information protection at the
enterprises of various levels including the strategic
appointment. The project implementation of John Pollard’s
factorization ρ–method in the programming language C ++ is
presented, which works faster than the standard algorithm by
27%. It can facilitate greatly the deciphering operation ...
Added: May 10, 2023
Черкесова Л. В., Сафарьян О. А., Смирнов И. А., Молодой исследователь Дона 2018 Т. 3 (12) С. 111–121
The paper presents the project implementation of ρ-factor Pollard factorization in C ++, which works faster than the standard algorithm by 27%, which can significantly facilitate the work in deciphering and cryptanalysis of various ciphers such as RSA ...
Added: May 9, 2023
Stepan L. Kuznetsov, Journal of Logic and Computation 2023 Vol. 33 No. 6 P. 1437–1462
We prove undecidability and pinpoint the place in the arithmetical hierarchy for commutative action logic, i.e. the equational theory of commutative residuated Kleene lattices (action lattices), and infinitary commutative action logic, the equational theory of *-continuous commutative action lattices. Namely, we prove that the former is Σ01�10-complete and the latter is Π01�10-complete. Thus, the situation is the ...
Added: March 7, 2023
Faliszewski P., Karpov A., Obraztsova S., Autonomous Agents and Multi-Agent Systems 2022 Vol. 36 Article 18
We analyze the complexity of several NP-hard election-related problems under the assumptions that the voters have group-separable preferences. We show that under this assumption our problems typically remain NP-hard, but we provide more efficient algorithms if additionally the clone decomposition tree is of moderate height. We also show a polynomial-time algorithm for sampling group-separable elections uniformly at ...
Added: March 14, 2022
Kanovich M., Kuznetsov S., Scedrov A. et al., Cambridge University Press, 2019.
Mathematical Structures in Computer Science is a journal of theoretical computer science which focuses on the application of ideas from the structural side of mathematics and mathematical logic to computer science. The journal aims to bridge the gap between theoretical contributions and software design, publishing original papers of a high standard and broad surveys with ...
Added: February 5, 2021
Kuznetsov S., , in: Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th BirthdayIssue 12300.: Cham: Springer, 2020. P. 3–16.
Infinitary action logic is an extension of the multiplicative-additive Lambek calculus with Kleene iteration, axiomatized by an 𝜔-rule. Buszkowski and Palka (2007) show that this logic is \(\Pi^0_1\)-complete. As shown recently by Kuznetsov and Speranski, the extension of infinitary action logic with the exponential modality is much harder: \(\Pi^1_1\)-complete. The raise of complexity is of ...
Added: November 25, 2020
IEEE Computer Society, 2018.
23rd IEEE FRUCT Conference. ...
Added: November 1, 2020
Novosibirsk: IEEE, 2018.
Added: April 23, 2019
Brotherston J., Kanovich M., , 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.
Added: December 5, 2018
Netherlands: Springer, 2018.
The 16th Asian Symposium on Programming Languages and Systems (APLAS) aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia but is an international forum that serves the worldwide programming languages community. APLAS 2018 ...
Added: December 5, 2018
IEEE Computer Society, 2017.
PROCEEDINGS
2017 Fourth International Conference on Engineering and Telecommunication ...
Added: October 4, 2018
Shitov Y., SIAM Review 2017 Vol. 59 No. 4 P. 794–800
Using elementary linear algebra, we develop a technique that leads to solutions of two widely known problems on nonnegative matrices. First, we give a short proof of the result by Vavasis stating that the nonnegative rank of a matrix is NP-hard to compute. This proof is essentially contained in the paper by Jiang and Ravikumar, ...
Added: November 9, 2017
Zakharyaschev M., BRESOLIN D., KURUCZ A. et al., , 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 ...
Added: September 17, 2017
Kanovich M., Brotherston J., Gorogiannis N., , in: 26th International Conference on Automated Deduction – CADE 26.: Springer, 2017. P. 472–490.
We investigate array separation logic (ASL), a variant of symbolic-heap separation logic in which the data structures are either pointers or arrays, i.e., contiguous blocks of memory. This logic provides a language for compositional memory safety proofs of array programs. We focus on the biabduction problem for this logic, which has been established as the key to automatic specification inference ...
Added: September 14, 2017
Brotherston J., Gorogiannis N., Kanovich Max et al., , 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 ...
Added: June 9, 2016
Zakharov V., Новикова Т. А., , 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.
It is generally accepted that to unify a pair of substitutions 1 and 2 means to find out
a pair of substitutions 0 and 00 such that the compositions 10 and 200 are the same.
Actually, unification is the problem of solving linear equations of the form 1X = 2Y in
the semigroup of substitutions. But some other ...
Added: October 13, 2015
Zakharov V.A., Kuzurin N. N., Varnovsky N. P. et al., 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 ...
Added: October 13, 2015
Zakharov V., Волканов Д. Ю., Зорин Д. А. et al., Программирование 2015 № 6 С. 72–86
Проверка правильности функционирования распределенных программ --- это одна из наиболее трудных и актуальных задач современного программирования. В статье описано комбинированное программно-инструментальное средство верификации распределенных вычислительных систем реального времени (РВС РВ). Для описания РВС РВ используется универсальный язык моделирования UML. Семантика диаграмм состояний UML определяется на основе модели вычислений иерархических временных автоматов. Средство верификации диаграмм UML ...
Added: October 13, 2015
Zakharov V., Коннов И. В., Journal of symbolic computation 2010 Vol. 45 No. 11 P. 1144–1162
A uniform verification problem for parameterized systems is to determine whether a temporal property is satisfied for every instance of the system which is composed of an arbitrary number of homogeneous processes. To cope with this problem we combine an induction-based technique for invariant generation and conventional model checking of finite state systems. At the ...
Added: October 12, 2015
Kanovich M., Ban Kirigin T., Nigam V. et al., , in: Lecture Notes in Computer Science. Computer Security – ESORICS 2013 18th European Symposium on Research in Computer Security, Egham, UK, September 9-13, 2013. Proceedings.: Berlin: Springer, 2013. Ch. 18 P. 309–326.
It is well-known that the Dolev-Yao adversary is a powerful adversary. Besides acting as the network, intercepting, sending, and composing messages, he can remember as much information as he needs. That is, his memory is unbounded.
We recently proposed a weaker Dolev-Yao like adversary, which also acts as the network, but whose memory is bounded. We ...
Added: March 24, 2015