?
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.
Brotherston J., Kanovich M., Journal of the ACM 2014 Vol. 61 No. 2 P. 14:1-14:43
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism ...
Added: March 23, 2015
Savateev Y., Annals of Pure and Applied Logic 2012 Vol. 163 P. 775-788
In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. Also we introduce a new derivability characterization for these calculi. ...
Added: October 20, 2014
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
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
Смирнов И. А., Разумов П. В., Болдырихин Н. В. 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
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., Information and Computation 2014 No. 238 P. 233-261
In a collaborative system, the agents collaborate to achieve a common goal, but they are not willing to share some sensitive private information.
The question is how much damage can be done by a malicious participant sitting inside the system.
We assume that all the participants (including internal adversaries) have bounded memory – at any moment, they ...
Added: March 23, 2015
Berlin : Springer, 2013
This volume contains the papers selected for presentation at the 18th European Symposium on Research in Computer Security (ESORICS 2013), held during September 9–13, 2013, in Egham, UK. In response to the symposium’s call for papers, 242 papers were submitted to the conference from 38 countries. These papers were evaluated on the basis of their ...
Added: March 24, 2015
Kanovich M., Ban Kirigin T., Nigam V. et al., Computer Languages, Systems & Structures 2014 No. 40 P. 137-154
It is well-known that the Dolev–Yao adversary is a powerful adversary. Besides acting as the network, intercepting, decomposing, composing and sending 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 ...
Added: March 23, 2015
Черкесова Л. В., Сафарьян О. А., Смирнов И. А., Молодой исследователь Дона 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
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
Kuznetsov S., , in : Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday. Issue 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
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
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
Savateev Y., Известия РАН. Серия математическая 2011 Т. 75 № 3 С. 189-222
We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents. ...
Added: October 20, 2014
IEEE Computer Society, 2018
23rd IEEE FRUCT Conference. ...
Added: November 1, 2020
Zakharov V., Кузюрин Н. Н., Варновский Н. П. et al., Программирование 2015 № 6
Program obfuscation is a semantic-preserving transformation aimed at bringing a program into such a form, which impedes the understanding of its algorithm and data structures or prevents extracting of some valuable information from the text of a program. Since obfuscation could find wide use in computer security, information hiding and cryptography, security requirements to program ...
Added: October 13, 2015
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
IEEE Computer Society, 2017
PROCEEDINGS
2017 Fourth International Conference on Engineering and Telecommunication ...
Added: October 4, 2018
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
Novosibirsk : IEEE, 2018
Added: April 23, 2019
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
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