8 citations · 17 across the 11 of their papers we have counts for
8 papers · 1 filter
General Decidability Results for Systems with Continuous Counters
A. R. Balasubramanian, Matthew Hague, Rupak Majumdar +2
Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs.…
Reachability in Continuous Pushdown VASS
A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam +1
Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but n…
Checking Refinement of Asynchronous Programs against Context-Free Specifications
Pascal Baumann, Moses Ganardi, Rupak Majumdar +2
In the language-theoretic approach to refinement verification, we check that the language of traces of an implementation all belong to the language of a specification. We consider…
Context-Bounded Verification of Thread Pools
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam +1
Thread pooling is a common programming idiom in which a fixed set of worker threads are maintained to execute tasks concurrently. The workers repeatedly pick tasks and execute them…
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche
The model of asynchronous programming arises in many contexts, from low-level systems software to high-level web programming. We take a language-theoretic perspective and show gene…
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam +1
We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that c…
The complexity of bounded context switching with dynamic thread creation
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam +1
Dynamic networks of concurrent pushdown systems (DCPS) are a theoretical model for multi-threaded recursive programs with shared global state and dynamical creation of threads. The…
Regular Separability and Intersection Emptiness are Independent Problems
Ramanathan S. Thinniyam, Georg Zetzsche
The problem of \emph{regular separability} asks, given two languages and , whether there exists a regular language with and . This prob…