| 2026 | CONCUR | Monadic Presburger Predicates Have Robust Population Protocols. | Philipp Czerner, Javier Esparza, Vincent Fischer, Roland Guttenberg, Julian Pins, Simon Reilich |
| 2025 | MFCS | Regular Model Checking for Systems with Effectively Regular Reachability Relation. | Javier Esparza, Valentin Krasotin |
| 2025 | RV | Runtime Verification for LTL in Stochastic Systems. | Javier Esparza, Vincent Fischer |
| 2025 | TACAS | Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification. | Michael Blondin, Michal Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza, Jakob Schulz |
| 2024 | CONCUR | Computing Inductive Invariants of Regular Abstraction Frameworks. | Philipp Czerner, Javier Esparza, Valentin Krasotin, Christoph Welzel-Mohr |
| 2024 | CONCUR | Validity of Contextual Formulas. | Javier Esparza, Rubn Rubio |
| 2024 | FOSSACS | A Resolution-Based Interactive Proof System for UNSAT. | Philipp Czerner, Javier Esparza, Valentin Krasotin |
| 2023 | CAV | Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms. | Eszter Couillard, Philipp Czerner, Javier Esparza, Rupak Majumdar |
| 2023 | CONCUR | Geometry of Reachability Sets of Vector Addition Systems. | Roland Guttenberg, Mikhail A. Raskin, Javier Esparza |
| 2023 | ICALP | Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems. | Javier Esparza, Vincent P. Grande |
| 2022 | CONCUR | Regular Model Checking Upside-Down: An Invariant-Based Approach. | Javier Esparza, Mikhail A. Raskin, Christoph Welzel |
| 2022 | FOSSACS | Separators in Continuous Petri Nets. | Michael Blondin, Javier Esparza |
| 2021 | CONCUR | Enforcing ω-Regular Properties in Markov Chains by Restarting. | Javier Esparza, Stefan Kiefer, Jan Kretnsk, Maximilian Weininger |
| 2021 | FOSSACS | Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy. | A. R. Balasubramanian, Javier Esparza, Mikhail A. Raskin |
| 2021 | PODC | Lower Bounds on the State Complexity of Population Protocols. | Philipp Czerner, Javier Esparza |
| 2021 | PODC | Decision Power of Weak Asynchronous Models of Distributed Computing. | Philipp Czerner, Roland Guttenberg, Martin Helfrich, Javier Esparza |
| 2020 | ATVA | Complexity of Verification and Synthesis of Threshold Automata. | A. R. Balasubramanian, Javier Esparza, Marijana Lazic |
| 2020 | ATVA | Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs. | Javier Esparza, Martin Helfrich, Stefan Jaax, Philipp J. Meyer |
| 2020 | CAV | Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. | Michael Blondin, Javier Esparza, Martin Helfrich, Antonn Kucera, Philipp J. Meyer |
| 2020 | CONCUR | A Classification of Weak Asynchronous Models of Distributed Computing. | Javier Esparza, Fabian Reiter |
| 2020 | CONCUR | Flatness and Complexity of Immediate Observation Petri Nets. | Mikhail A. Raskin, Chana Weil-Kennedy, Javier Esparza |
| 2020 | LICS | An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata. | Salomon Sickert, Javier Esparza |
| 2020 | STACS | Succinct Population Protocols for Presburger Arithmetic. | Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, Stefan Jaax |
| 2020 | TACAS | Structural Invariants for the Verification of Systems with Parameterized Architectures. | Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, Christoph Welzel |
| 2019 | CONCUR | Expressive Power of Broadcast Consensus Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax |
| 2019 | TACAS | Computing the Expected Execution Time of Probabilistic Workflow Nets. | Philipp J. Meyer, Javier Esparza, Philip Offtermatt |
| 2018 | CAV | Peregrine: A Tool for the Analysis of Population Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax |
| 2018 | CONCUR | Automatic Analysis of Expected Termination Time for Population Protocols. | Michael Blondin, Javier Esparza, Antonn Kucera |
| 2018 | CONCUR | Verification of Immediate Observation Population Protocols. | Javier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy |
| 2018 | LICS | Black Ninjas in the Dark: Formal Analysis of Population Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax, Antonn Kucera |
| 2018 | LICS | One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. | Javier Esparza, Jan Kretnsk, Salomon Sickert |
| 2018 | STACS | Large Flocks of Small Birds: on the Minimal Size of Population Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax |
| 2018 | TACAS | Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets. | Philipp J. Meyer, Javier Esparza, Hagen Vlzer |
| 2017 | CSR | Advances in Parameterized Verification of Population Protocols. | Javier Esparza |
| 2017 | LICS | Static analysis of deterministic negotiations. | Javier Esparza, Anca Muscholl, Igor Walukiewicz |
| 2017 | PODC | Towards Efficient Verification of Population Protocols. | Michael Blondin, Javier Esparza, Stefan Jaax, Philipp J. Meyer |
| 2017 | TACAS | From LTL and Limit-Deterministic Bchi Automata to Deterministic Parity Automata. | Javier Esparza, Jan Kretnsk, Jean-Franois Raskin, Salomon Sickert |
| 2017 | TIME | Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk). | Javier Esparza |
| 2016 | CAV | Limit-Deterministic Bchi Automata for Linear Temporal Logic. | Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Kretnsk |
| 2016 | CONCUR | Soundness in Negotiations. | Javier Esparza, Denis Kuperberg, Anca Muscholl, Igor Walukiewicz |
| 2016 | FASE | Reduction Rules for Colored Workflow Nets. | Javier Esparza, Philipp Hoffmann |
| 2015 | CAV | Model Checking Parameterized Asynchronous Shared-Memory Systems. | Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty, Rupak Majumdar |
| 2015 | CONCUR | Verification of Population Protocols. | Javier Esparza, Pierre Ganty, Jrme Leroux, Rupak Majumdar |
| 2015 | FMCAD | An SMT-based Approach to Fair Termination Analysis. | Javier Esparza, Philipp J. Meyer |
| 2015 | VMCAI | Distributed Markov Chains. | Ratul Saha, Javier Esparza, Sumit Kumar Jha, Madhavan Mukund, P. S. Thiagarajan |
| 2014 | CAV | From LTL to Deterministic Automata: A Safraless Compositional Approach. | Javier Esparza, Jan Kretnsk |
| 2014 | CAV | An SMT-Based Approach to Coverability Analysis. | Javier Esparza, Rusln Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic |
| 2014 | CONCUR | Deterministic Negotiations: Concurrency for Free. | Javier Esparza |
| 2014 | EACL | Fast and Accurate Unlexicalized Parsing via Structural Annotations. | Maximilian Schlund, Michael Luttenberger, Javier Esparza |
| 2014 | FOSSACS | On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations. | Javier Esparza, Jrg Desel |
| 2014 | LATA | A Brief History of Strahler Numbers. | Javier Esparza, Michael Luttenberger, Maximilian Schlund |
| 2014 | STACS | Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk). | Javier Esparza |
| 2014 | VMCAI | Message-Passing Algorithms for the Verification of Distributed Protocols. | Log Jezequel, Javier Esparza |
| 2013 | CAV | Parameterized Verification of Asynchronous Shared-Memory Systems. | Javier Esparza, Pierre Ganty, Rupak Majumdar |
| 2013 | CAV | A Fully Verified Executable LTL Model Checker. | Javier Esparza, Peter Lammich, Ren Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus |
| 2013 | CONCUR | On Negotiation as Concurrency Primitive. | Javier Esparza, Jrg Desel |
| 2012 | ATVA | Rabinizer: Small Deterministic Automata for LTL(F, G). | Andreas Gaiser, Jan Kretnsk, Javier Esparza |
| 2012 | CAV | Proving Termination of Probabilistic Programs Using Patterns. | Javier Esparza, Andreas Gaiser, Stefan Kiefer |
| 2012 | CAV | Deterministic Automata for the (F, G)-Fragment of LTL. | Jan Kretnsk, Javier Esparza |
| 2012 | LICS | A Perfect Model for Bounded Verification. | Javier Esparza, Pierre Ganty, Rupak Majumdar |
| 2011 | CALCO | Solving Fixed-Point Equations by Derivation Tree Analysis. | Javier Esparza, Michael Luttenberger |
| 2011 | POPL | Complexity of pattern-based verification for multithreaded programs. | Javier Esparza, Pierre Ganty |
| 2011 | SAS | Probabilistic Abstractions with Arbitrary Domains. | Javier Esparza, Andreas Gaiser |
| 2010 | FMICS | Automatic Error Correction of Java Programs. | Christian Kern, Javier Esparza |
| 2010 | ICALP | Space-Efficient Scheduling of Stochastically Generated Tasks. | Toms Brzdil, Javier Esparza, Stefan Kiefer, Michael Luttenberger |
| 2010 | STACS | Computing Least Fixed Points of Probabilistic Systems of Polynomials. | Javier Esparza, Andreas Gaiser, Stefan Kiefer |
| 2010 | VMCAI | Analysis of Systems with Stochastic Process Creation. | Javier Esparza |
| 2009 | MFCS | Stochastic Process Creation. | Javier Esparza |
| 2008 | DLT | Derivation Tree Analysis for Accelerated Fixed-Point Computation. | Javier Esparza, Stefan Kiefer, Michael Luttenberger |
| 2008 | ICALP | Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations. | Javier Esparza, Thomas Gawlitza, Stefan Kiefer, Helmut Seidl |
| 2008 | ICALP | Newton's Method for omega-Continuous Semirings. | Javier Esparza, Stefan Kiefer, Michael Luttenberger |
| 2008 | STACS | Convergence Thresholds of Newton's Method for Monotone Polynomial Equations. | Javier Esparza, Stefan Kiefer, Michael Luttenberger |
| 2008 | TACAS | SDSIrep: A Reputation System Based on SDSI. | Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth |
| 2007 | CAV | jMoped: A Test Environment for Java Programs. | Dejvuth Suwimonteerabuth, Felix Berger, Stefan Schwoon, Javier Esparza |
| 2007 | DLT | An Extension of Newton's Method to | Javier Esparza, Stefan Kiefer, Michael Luttenberger |
| 2007 | STOC | On the convergence of Newton's method for monotone systems of polynomial equations. | Stefan Kiefer, Michael Luttenberger, Javier Esparza |
| 2007 | STACS | On Fixed Point Equations over Commutative Semirings. | Javier Esparza, Stefan Kiefer, Michael Luttenberger |
| 2006 | ATVA | Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. | Giorgio Delzanno, Javier Esparza, Jir Srba |
| 2006 | ATVA | Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains. | Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza |
| 2006 | TACAS | Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems. | Javier Esparza, Stefan Kiefer, Stefan Schwoon |
| 2005 | FOCS | Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion (Extended Abstract). | Toms Brzdil, Javier Esparza, Antonn Kucera |
| 2005 | LICS | Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances. | Javier Esparza, Antonn Kucera, Richard Mayr |
| 2005 | SAS | Locality-Based Abstractions. | Javier Esparza, Pierre Ganty, Stefan Schwoon |
| 2005 | TACAS | A Note on On-the-Fly Verification Algorithms. | Stefan Schwoon, Javier Esparza |
| 2005 | TACAS | jMoped: A Java Bytecode Checker Based on Moped. | Dejvuth Suwimonteerabuth, Stefan Schwoon, Javier Esparza |
| 2004 | LICS | Model Checking Probabilistic Pushdown Automata. | Javier Esparza, Antonn Kucera, Richard Mayr |
| 2003 | CONCUR | Synthesis of Distributed Algorithms Using Asynchronous Automata. | Alin Stefanescu, Javier Esparza, Anca Muscholl |
| 2003 | DLT | An Automata-Theoretic Approach to Software Verification. | Javier Esparza |
| 2003 | POPL | A generic approach to the static analysis of concurrent programs with procedures. | Ahmed Bouajjani, Javier Esparza, Tayssir Touili |
| 2003 | TACAS | Simple Representative Instantiations for Multicast Protocols. | Javier Esparza, Monika Maidl |
| 2002 | SAS | An Algebraic Approach to the Static Analysis of Concurrent Software. | Javier Esparza |
| 2001 | CAV | A BDD-Based Model Checker for Recursive Programs. | Javier Esparza, Stefan Schwoon |
| 2001 | PPDP | Model Checking (with) Declarative Programs. | Javier Esparza |
| 2000 | CAV | Efficient Algorithms for Model Checking Pushdown Systems. | Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon |
| 2000 | ICALP | A New Unfolding Approach to LTL Model Checking. | Javier Esparza, Keijo Heljanko |
| 2000 | MFCS | Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL. | Leonor Prensa Nieto, Javier Esparza |
| 2000 | POPL | Efficient Algorithms for pre | Javier Esparza, Andreas Podelski |
| 1999 | CONCUR | An Unfolding Algorithm for Synchronous Products of Transition Systems. | Javier Esparza, Stefan Rmer |
| 1999 | CONCUR | Proof-Checking Protocols Using Bisimulations. | Christine Rckl, Javier Esparza |
| 1999 | CSL | Constraint-Based Analysis of Broadcast Protocols. | Giorgio Delzanno, Javier Esparza, Andreas Podelski |
| 1999 | CSL | A Logical Viewpoint on Process-Algebraic Quotients. | Antonn Kucera, Javier Esparza |
| 1999 | FOSSACS | An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis. | Javier Esparza, Jens Knoop |
| 1999 | LICS | On the Verification of Broadcast Protocols. | Javier Esparza, Alain Finkel, Richard Mayr |
| 1997 | CONCUR | Reachability Analysis of Pushdown Automata: Application to Model-Checking. | Ahmed Bouajjani, Javier Esparza, Oded Maler |
| 1996 | ESOP | Checking System Properties via Integer Programming. | Stephan Melzer, Javier Esparza |
| 1996 | ICALP | An Effective Tableau System for the Linear Time µ-Calculus. | Julian C. Bradfield, Javier Esparza, Angelika Mader |
| 1996 | ICALP | Deciding Finiteness of Petri Nets Up To Bisimulation. | Petr Jancar, Javier Esparza |
| 1996 | TACAS | An Improvement of McMillan's Unfolding Algorithm. | Javier Esparza, Stefan Rmer, Walter Vogler |
| 1995 | CAV | On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes. | Javier Esparza, Astrid Kiehn |
| 1995 | FCT | Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes. | Javier Esparza |
| 1994 | CONCUR | Operational Semantics for the Petri Box Calculus. | Maciej Koutny, Javier Esparza, Eike Best |
| 1993 | STACS | General Refinement and Recursion Operators for the Petri Box Calculus. | Eike Best, Raymond Devillers, Javier Esparza |
| 1993 | WG | The Asynchronous Committee Meeting Problem. | Javier Esparza, Bernhard von Stengel |
| 1991 | CONCUR | Compositional Synthesis of Live and Bounded Free Choice Petri Nets. | Javier Esparza, Manuel Silva Surez |
| 1991 | CSL | Model Checking of Persistent Petri Nets. | Eike Best, Javier Esparza |
| 1991 | STACS | Reachability in Reversible Free Choice Systems. | Jrg Desel, Javier Esparza |
| 1990 | CONCUR | Synthesis Rules for Petri Nets, and How they Lead to New Results. | Javier Esparza |