SDSIrep: A Reputation System based on SDSI (TACAS'08 paper with Bouajjani, Schwoon, Suwimonteerabuth)
Derivation Tree Analysis for Accelerated Fixed-Point Computation (DLT'08 paper with Kiefer, Luttenberger)
Symbolic Context-Bounded Analysis of Multithreaded Java Programs (SPIN'08 paper with Suwimonteerabuth, Schwoon)
Solving Monotone Polynomial Equations (TCS'08 paper with Kiefer, Luttenberger)
Newton's Method for 
-Continuous Semirings (ICALP'08 paper with Kiefer, Luttenberger)
Approximative Methods for Monotone Systems of min-max-Polynomial Equations (ICALP'08 paper with Gawlitza, Kiefer, Seidl)
Convergence Thresholds of Newton's Method for Monotone Polynomial Equations (STACS'08 paper with Kiefer, Luttenberger)
jMoped: A Test Environment for Java programs (CAV'07 paper with Suwimonteerabuth, Berger, Schwoon)
On the Convergence of Newton's Method for Monotone Systems of Polynomial Equations (STOC'07 paper with Kiefer, Luttenberger)
An Extension of Newton's Method to -Continuous Semirings (DLT'07 paper with Kiefer, Luttenberger)
On Fixed Point Equations over Commutative Semirings (STACS'07 paper with Kiefer, Luttenberger)
Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains (ATVA'06 paper with Suwimonteerabuth, Schwoon)
On the Complexity of Consistency and Complete State Coding (ACSD'06 paper with Jančar, Miller)
,
Rewriting Models of Boolean Programs (RTA'06 paper with Bouajjani)
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols (ATVA'06 paper with Delzanno, Srba)
Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems (TACAS'06 paper with Kiefer, Schwoon)
Reachability analysis of multithreaded software with asynchronous communication (FSTTCS'05 paper with Bouajjani, Schwoon, Strejček)
A Note on On-The-Fly Verification Algorithms (TACAS'05 paper with Schwoon)
jMoped: A Java bytecode checker based on Moped (TACAS'05 paper with Suwimonteerabuth, Schwoon)
Analysis and Prediction of the Long-run Behaviour of Probabilistic Sequential Programs with Recursion (FOCS'05 paper with Brádzil, Kučera)
Locality-based Abstractions (SAS'05 paper with Ganty, Schwoon)
Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances (LICS 2005 paper with Kučera, Mayr)
Verifying probabilistic procedural programs (FSTTCS'04 paper with Etessami)
Reachability Analysis of Synchronized PA-Systems (Infinity'04 paper with Bouajjani, Touili)
Model Checking Probabilistic Pushdown Automata (LICS'04 paper with Kučera, Mayr)
,
A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs (ACSD'03)
Synthesis of Distributed Algorithms Using Asynchronous Automata (CONCUR'03 paper with Ștefănescu, Muscholl)
A Generic Approach to the Static Analysis of Concurrent Programs with Procedures (POPL'93 paper with Bouajjani, Touili)
Simple Representative Instantiations for Multicast Protocols (TACAS'03 paper with Maidl)
Grammars as Processes (Formal and Natural Computing 2002)
The Model-Checking Kit (satellite event of CONCUR'09 paper with Schröter, Schwoon)
Implementing LTL Model Checking with Net Unfoldings (SPIN'01 paper with Heljanko)
A BDD-based Model Checker for Recursive Programs (CAV'01 paper with Schwoon)
Net Reductions for LTL Model-Checking (CHARME'01 paper with Schröter)
Model-Checking LTL with Regular Valuations for Pushdown Systems (TACS'01 paper with Kučera, Schwoon)
A New Unfolding Approach to LTL Model Checking (CALP'00 paper with Heljanko)
Efficient Algorithms for Model Checking Pushdown Systems (CAV'00 paper with Hansel, Rossmanith, Schwoon)
Efficient Algorithms for it pre
and it post on Interprocedural Parallel Flow Graphs (POPL'00 paper with Podelski)
Reachability Analysis Using Net Unfoldings (Workshop of Concurrency, Specification & Programming 2000 paper with Schröter)
Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL (Conference on Mathematical Foundations of Computer Science 2000 paper with Nieto)
On the Mechanized Verification of Infinite Systems (SFB 342 Final Colloquium 2000 paper with Röckl)
Constraint-based Analysis of Broadcast Protocols (CSL'99 paper with Delzanno, Podelski)
On the Verification of Broadcast Protocols (LICS'99 paper with Finkel, Mayr)
An Automata-theoretic Approach to Interprocedural Dataflow Analysis (FOSSACS'99 paper with Knoop)
An Unfolding Algorithm for Synchronous Products of Transition Systems (CONCUR'99 paper with Römer)
A logical viewpoint on process-algebraic quotients (CSL'99 paper with Kučera)
Proof-Checking Protocols Using Bisimulations (CONCUR'99 paper with Röckl)
Decidability and Complexity of Petri Net Problems – an Introduction (Advances in Petri Nets 1998)
The PEP Verification System (FEmSys'97 paper with Best, Grahlmann, Melzer, Römer, Wallner)
Reachability Analysis of Pushdown Automata: Application to Model-Checking (CONCUR'97 paper with Bouajjani, Maler)
Model Checking LTL using Constraint Programming (Application and Theory of Petri Nets 1997 paper with Melzer)
An Automata Approach to Some Problems on Context-free Grammars (Foundations of Computer Science, Potential - Theory - Cognition 1997 paper with Rossmanith)
An effective tableau system for the linear time mu-calculus (ICALP'96 paper with Bradfield, Mader)
An Improvement of McMillan's Unfolding Algorithm (TACAS'96 paper with Römer, Vogler)
More Infinite Results (INFINITY'96)
Deciding finiteness of Petri nets up to bisimulation (ICALP'96 paper with Jancar)
A Polynomial Algorithm to Compute the Concurrency Relation of Free-Choice Signal Transition Graphs (WODES'96 paper with Kovalyov)
Checking System Properties via Integer Programming (ESOP'96 paper with Melzer)
Verification Using PEP (Tool presentation) (AMAST'96 paper with Melzer, Römer)
On the model checking problem for branching time logics and Basic Parallel Processes (CAV'95 paper with Kiehn)
Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes (FCT'95)
On the Decidability of Model Checking for Several mu-calculi and Petri Nets (CAAP'94)
Operational Semantics for the Petri Box Calculus (CONCUR'94 paper with Koutny, Best)
General Refinement and Recursion Operators for the Petri Box Calculus (STACS'93 paper with Best, Devillers)
The Asynchronous Committee Meeting Problem (WG'93 paper with Stengel:)
Traps, Free Choice und Home States (extended abstract) (Semantics for Concurrency 1990 paper with Best, Cherkasova, Desel)
Model Checking of Persistent Petri Nets (CSL'91 paper with Best)
Reachability in Reversible Free Choice Systems (STACS'91 paper with Desel)
Top-Down Synthesis of Free Choice Nets (Advances in Petri Nets 1991 paper with Silva)
Compositional Synthesis of Live und Bounded Free Choice Nets (CONCUR'91 paper with Silva)
On the Analysis und Synthesis of Free Choice Systems (Advances in Petri Nets 1990 paper with Silva)
Circuits, Handles, Bridges and Nets (Advances in Petri Nets 1990 paper with Silva)
Synthesis Rules for Petri Nets, und How they Lead to New Results (CONCUR'90)