3 citations · 7 across the 6 of their papers we have counts for
8 papers · 1 filter
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…
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…
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…