2026-07-23T17:16:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18055 2024-03-06T11:00:53Z ddc:004 open_access

Context-Bounded Analysis of Concurrent Programs (Invited Talk) Baumann, Pascal Ganardi, Moses Majumdar, Rupak Thinniyam, Ramanathan S. Zetzsche, Georg Context-bounded analysis Multi-threaded programs Decidability Context-bounded analysis of concurrent programs is a technique to compute a sequence of under-approximations of all behaviors of the program. For a fixed bound k, a context bounded analysis considers only those runs in which a single process is interrupted at most k times. As k grows, we capture more and more behaviors of the program. Practically, context-bounding has been very effective as a bug-finding tool: many bugs can be found even with small bounds. Theoretically, context-bounded analysis is decidable for a large number of programming models for which verification problems are undecidable. In this paper, we survey some recent work in context-bounded analysis of multithreaded programs. In particular, we show a general decidability result. We study context-bounded reachability in a language-theoretic setup. We fix a class of languages (satisfying some mild conditions) from which each thread is chosen. We show context-bounded safety and termination verification problems are decidable iff emptiness is decidable for the underlying class of languages and context-bounded boundedness is decidable iff finiteness is decidable for the underlying class. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pascal Baumann and Moses Ganardi and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche 2023 Is Part Of LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2023.3 urn:nbn:de:0030-drops-180559 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.3 eng https://creativecommons.org/licenses/by/4.0/legalcode