?
Model checking for symbolic-heap separation logic with inductive predicates
P. 84–96.
Brotherston J., Gorogiannis N., Kanovich Max, Rowe R.
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 point algorithm that decides the problem and runs in exponential time in the size of the problem instance. Second, we show that, while model checking for the full language is EXPTIME-complete, the problem becomes NP-complete or PTIME-solvable when we impose natural syntactic restrictions on the schemata defining the inductive predicates. We additionally present NP and PTIME algorithms for these restricted fragments. Finally, we report on the experimental performance of our procedures on a variety of specifications extracted from programs, exercising multiple combinations of syntactic restrictions.
We are happy to be accepted to the POPL, one of the most prestigious conferencies in computer science.
In addition to that, our paper has been honored with the POPL stamp "Artefact evaluated" (see the attachment)
Yerbolova A. S., Tomashchuk K., Kogan A. et al., Complexity 2026 Vol. 2026 No. 1 Article 5519690
Tis paper presents a novel approach to analyzing and grouping natural languages based on the degree of their chaoticity. It clusters 52 languages from 18 language families, according to the value of the entropy–complexity pair, to reveal the chaotic properties of semantic trajectories. Te obtained clusters appear to be closely correlated with the family of ...
Added: February 16, 2026
Speranski S. O., Journal of Logic and Computation 2013 Vol. 23 No. 5 P. 1035–1055
In the present article, the quantifiers over propositions are first introduced into the language for reasoning about probability, then the complexity issues for validity problems dealing with the corresponding hierarchy of probabilistic sentences are investigated. We prove, among other things, the $\Pi^1_1$-completeness for the general validity and also indicate the least level in the hierarchy ...
Added: December 27, 2025
Speranski S. O., Computability 2015 Vol. 4 No. 2 P. 159–174
Added: December 27, 2025
Speranski S. O., Studia Logica 2017 Vol. 105 No. 2 P. 407–429
The paper contains a survey on the complexity of various truth hierarchies arising in Kripke’s theory. I present some new arguments, and use them to obtain a number of interesting generalisations of known results. These arguments are both relatively simple, involving only the basic machinery of constructive ordinals, and very general. ...
Added: December 26, 2025
Kuznetsov S., Speranski S. O., Annals of Pure and Applied Logic 2022 Vol. 173 No. 2 Article 103057
We introduce infinitary action logic with exponentiation — that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allow some of the structural rules (contraction, weakening, permutation). The logic is presented in the form of an infinitary sequent calculus. We prove cut elimination and, in the case ...
Added: December 26, 2025
Kuznetsov S., Speranski S. O., Studia Logica 2023 Vol. 111 No. 2 P. 251–280
Infinitary action logic can be naturally expanded by adding exponential and subexponential modalities from linear logic. In this article we shall develop infinitary action logic with a subexponential that allows multiplexing (instead of contraction). Both non-commutative and commutative versions of this logic will be considered, presented as infinitary sequent calculi. We shall prove cut admissibility ...
Added: December 26, 2025
Speranski S. O., Logic Journal of the IGPL 2025 Vol. 33 No. 2 Article jzae042
This paper is concerned with a two-sorted probabilistic language, denoted by QPL, which contains quantifiers over events and over reals, and can be viewed as an elementary language for reasoning about probability spaces. The fragment of QPL containing only quantifiers over reals is a variant of the well-known ‘polynomial’ language from [Fagin et al. 1990, Section 6]. ...
Added: December 26, 2025
Speranski S. O., Logic Journal of the IGPL 2025 Vol. 33 No. 3 Article jzae114
We shall be concerned with two natural expansions of the quantifier-free ‘polynomial’ probability logic of [Fagin et al. 1990]. One of these, denoted by QPL-e, is obtained by adding quantifiers over arbitrary events, and the other, denoted by p-QPL-e, uses quantifiers over propositional formulas — or equivalently, over events expressible by such formulas. The earlier proofs ...
Added: December 26, 2025
LePoire D., Grinin L. E., Korotayev A., Journal of Big History 2025 Vol. 8 No. 3 P. 98–139
Building on foundational work in systems theory, thermodynamics, and evolutionary theory, this paper argues that complexity can serve as a conceptual bridge across disciplines. It explores the role of complexity dynamics in Big History through an integrative theoretical framework that spans physical, chemical, geological, biological, social, cognitive, and civilizational domains. By examining how complexity emerges, ...
Added: November 1, 2025
Yury Semenov, Oleg Sukhoroslov, , in: Mathematical Optimization Theory and Operations Research 24th International Conference, MOTOR 2025, Novosibirsk, Russia, July 7–11, 2025, ProceedingsVol. 15681.: Switzerland: Springer, 2025. P. 317–331.
Added: September 17, 2025
Arzhantsev I., Functional Analysis and Its Applications 1997 Vol. 31 No. 4 P. 278–280
Let a connected reductive group G act on a normal affine variety X with the generic stabilizer H, let the complexity of this action be one, and let the categorial quotient X//G be one-dimensional. Then the closure of any G-orbit in X is normal. ...
Added: June 13, 2025
Cham: Springer, 2020.
This book highlights cutting-edge research in the field of network science, offering scientists, researchers, students, and practitioners a unique update on the latest advances in theory and a multitude of applications. It presents the peer-reviewed proceedings of the Eighth International Conference on Complex Networks and their Applications (COMPLEX NETWORKS 2019), which took place in Lisbon, ...
Added: February 27, 2024
Marina Boykova, Knyazeva H., Salazkin M., Foresight and STI Governance 2023 Vol. 17 No. 4 P. 80–91
The challenges the futures studies face are particularly complex, interconnected, and contradictory, and cannot be resolved using linear approaches. Prognostic science needs tools matching the new contextual complexity, which would allow to capture a much wider range of driving forces, and their potential effects, in a non-linear perspective, to improve the accuracy of forecasts and ...
Added: January 25, 2024
Springer, 2021.
Springer Proceedings in Complexity publishes proceedings from scholarly meetings on all topics relating to the interdisciplinary studies of complex systems science. Springer welcomes book ideas from authors. The series is indexed in Scopus ...
Added: January 15, 2023
Perez-Guerra J., Smirnova E. A., VIAL - Vigo International Journal of Applied Linguistics 2023 No. 20 P. 149–183
This study focuses on the analysis of linguistic complexity in professional academic writing in light of the empirical evidence provided by a 1,597,000-word corpus of ‘hard’ (life and physical sciences) and ‘soft’ (arts and social) scientific research articles published in leading peer-review journals. Specifically, this investigation aims both to describe the complexity features of texts ...
Added: December 20, 2022
Gromov V., Мазайшвили К. В., Заикин П. В. et al., Вестник кибернетики 2022 Т. 45 № 1 С. 72–82
The prevalence of chronic kidney disease is growing every year and is already comparable to such socially significant diseases as hypertension and diabetes mellitus, as well as obesity and metabolic syndrome [1,2]. The standard solution for hemodialysis patients is to create a permanent vascular access in the form of an arteriovenous fistula. However, its use ...
Added: November 14, 2022
Science and Technology Publications, Lda, 2022.
This book contains the proceedings of the 7th International Conference on Complexity, Future Information Systems and Risk (COMPLEXIS 2022), which was organized and sponsored by the Institute for Systems and Technologies of Information, Control and Communication (INSTICC). This year COMPLEXIS was held as a web-based event due to the COVID-19 pandemic, from 23 to 24 ...
Added: September 8, 2022
Springer, 2022.
Springer Proceedings in Complexity publishes proceedings from scholarly meetings on all topics relating to the interdisciplinary studies of complex systems science. Springer welcomes book ideas from authors. The series is indexed in Scopus. ...
Added: July 13, 2022
INDAUTOR, 2021.
Ciencia jurídica, transdisciplina y complejidad. Tendencias para la innovación para el aprendizaje jurídico, se centra en el aprendizaje a lo largo d$e la vida para toda persona, propone una inversión sin precedentes en el trabajo colaborativo para lograr la mayor eficacia del modelo de convivencia vanguardista que representan los derechos, deberes y libertades fundamentales, orientados ...
Added: February 10, 2022
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Sequential reactive systems include programs and devices that work with two streams of
data and convert input streams of data into output streams. Such information processing systems
include controllers, device drivers, computer interpreters. The results of operation of such computing
systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite
transducers are most often ...
Added: January 17, 2022
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification ...
Added: January 17, 2022
Bakhchina A., Apanovich V., Arutyunova K. et al., Frontiers in Psychology 2021 Vol. 12 Article 762225
Analytic and holistic thinking styles are known to be associated with individual differences in various aspects of behavior and brain activity. In this study, we tested a hypothesis that differences in thinking styles may also be manifested at the level of neuro-visceral coordination. Heart rate variability (HRV) was compared between analytic and holistic thinkers at ...
Added: January 12, 2022
Turchin P., Hoyer D., Korotayev A. et al., Plos One 2021 Vol. 16 No. 10 Article e0258161
What have been the causes and consequences of technological evolution in world history? In particular, what propels innovation and diffusion of military technologies, details of which are comparatively well preserved and which are often seen as drivers of broad socio-cultural processes? Here we analyze the evolution of key military technologies in a sample of pre-industrial ...
Added: November 7, 2021