Context-Bounded Analysis of Concurrent Programs (Invited Talk)
| Autor: | Baumann, Pascal, Ganardi, Moses, Majumdar, Rupak, Thinniyam, Ramanathan S., Zetzsche, Georg |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| DOI: | 10.4230/lipics.icalp.2023.3 |
| Popis: | 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. LIPIcs, Vol. 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), pages 3:1-3:16 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|