3 citations · 7 across the 6 of their papers we have counts for
10 papers
Bounded treewidth, multiple context-free grammars, and downward closures
C. Aiswarya, Pascal Baumann, Prakash Saivasan +2
The reachability problem in multi-pushdown automata (MPDA) has many applications in static analysis of recursive programs. An example is safety verification of multi-threaded recur…
Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities
Pascal Baumann, Eren Keskin, Roland Meyer +1
The omega-regular separability problem for Büchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper…
Monus semantics in vector addition systems with states
Pascal Baumann, Khushraj Madnani, Filip Mazowiecki +1
Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometime…
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…
Regular Separability in Büchi VASS
Pascal Baumann, Roland Meyer, Georg Zetzsche
We study the (-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages and , check whether there is a regular language that fully…
Unboundedness problems for machines with reversal-bounded counters
Pascal Baumann, Flavio D'Alessandro, Moses Ganardi +4
We consider a general class of decision problems concerning formal languages, called ``(one-dimensional) unboundedness predicates'', for automata that feature reversal-bounded coun…
Existential Definability over the Subword Ordering
Pascal Baumann, Moses Ganardi, Ramanathan S. Thinniyam +1
We study first-order logic (FO) over the structure consisting of finite words over some alphabet , together with the (non-contiguous) subword ordering. In terms of decidability…
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…
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…