Olzhas Zhangeldinov

dblp:329/5941 · DBLP profile ↗
← Back
3ranked-venue papers
0as first author
3since 2021 · last 2026
0009-0006-6381-9138ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 3 · 3 since 2021
YearPublicationVenuePosition
2026 CARET Model Checking of Self Modifying Code
Tayssir Touili, Olzhas Zhangeldinov
TASE2
2026 LTL model checking of concurrent self-modifying code
Tayssir Touili, Olzhas Zhangeldinov
J. Log. Algebraic Methods Program.2
2025 LTL Model Checking of Concurrent Self Modifying Code
abstract
We consider the LTL model-checking problem of concurrent self-modifying code, i.e., concurrent code that has the ability to modify its own instructions during execution time. This style of code is frequently utilized by malware developers to make their malicious code hard to detect. To model such programs, we consider Self-Modifying Dynamic Pushdown Networks (SM-DPN). A SM-DPN is a network of Self-Modifying Pushdown processes, where each process has the ability to modify its current set of rules and to spawn new processes during execution time. We consider model checking SM-DPNs against single indexed LTL formulas, i.e., conjunctions of separate LTL formulas on each single process. This problem is non-trivial since the number of spawned processes in a given run can be infinite. Our approach is based on computing finite automata representing the set of configurations from which the SM-DPN has a run that satisfies the single-indexed LTL formula. We implemented our techniques in a tool and obtained promising results. We demonstrate that our tool successfully detects concurrent and self-modifying malware.
Tayssir Touili, Olzhas Zhangeldinov
ICECCS2