Approach to static verification of multithreaded applications based on a graph model of a program

Approach to static verification of multithreaded applications based on a graph model of a program

Kryukov O.S. (TSU, Tula, Russia)
Voloshko A.G. (TSU, Tula, Russia)
Ivutin A.N. (TSU, Tula, Russia)

Abstract

This work is devoted to developing a static verification method for concurrent programs through the analysis of automatically constructed formal program models. The proposed solution is a graph-based approach utilizing an extended Petri net with semantic relations, which, owing to the explicit separation of control and data flows within a directed bipartite graph, enables efficient detection of critical concurrency errors, such as data races and deadlocks. The practical significance of the approach is confirmed by a prototype implementation – the Semantic Petri Net Analyzer for the Go language – which, in experiments conducted on the GoBench benchmark, demonstrated its ability to detect data races and deadlocks and outperformed dynamic analysis methods. It is shown that the proposed method offers a balanced solution for enhancing the reliability of concurrent software, combining analysis completeness, automation, and practical applicability.

Keywords

static verification; concurrent programs; Petri net; data race; deadlock; model checking.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 6, part 1, 2026, pp. 41-62

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-3

For citation

Kryukov O.S., Voloshko A.G., Ivutin A.N. Approach to static verification of multithreaded applications based on a graph model of a program. Proceedings of the Institute for System Programming, vol. 38, issue 6, part 1, 2026, pp. 41-62 DOI: 10.15514/ISPRAS-2026-38(6)-3.

Full text of the paper in pdf (in Russian) Back to the contents of the volume