Person: Javier Esparza

DBLP: Esparza:Javier

Facilitated 3 volumes:

Ed

Ed

Ed

Contributed to:

2015

2015

2014

2014

2014

2014

2014

2013

2012

2012

2011

2011

2010

2010

2010

2008

2008

2008

2008

2007

2007

2007

2006

2006

2005

2005

2005

2004

2003

2003

2003

2002

2001

2001

2000

2000

2000

1999

1999

1999

1996

1996

1996

1995

1991

1993

2016

2016

2018

Wrote 56 papers:

CAV-2015-Durand-Gasselin #model checking

Model Checking Parameterized Asynchronous Shared-Memory Systems (ADG, JE, PG, RM), pp. 67–84.

VMCAI-2015-SahaEJMT #distributed #markov

Distributed Markov Chains (RS, JE, SKJ, MM, PST), pp. 117–134.

CAV-2014-EsparzaK #approach #automaton #composition #ltl

From LTL to Deterministic Automata: A Safraless Compositional Approach (JE, JK), pp. 192–208.

CAV-2014-EsparzaLMMN #analysis #approach #smt

An SMT-Based Approach to Coverability Analysis (JE, RLG, RM, PM, FN), pp. 603–619.

CIAA-2014-EsparzaLS #equation #fixpoint #named

FPsolve: A Generic Solver for Fixpoint Equations over Semirings (JE, ML, MS), pp. 1–15.

FoSSaCS-2014-EsparzaD #concurrent #on the

On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations (JE, JD), pp. 258–273.

LATA-2014-EsparzaLS

A Brief History of Strahler Numbers (JE, ML, MS), pp. 1–13.

VMCAI-2014-JezequelE #algorithm #distributed #message passing #protocol #verification

Message-Passing Algorithms for the Verification of Distributed Protocols (LJ, JE), pp. 222–241.

CAV-2013-EsparzaGM #verification

Parameterized Verification of Asynchronous Shared-Memory Systems (JE, PG, RM), pp. 124–140.

CAV-2013-EsparzaLNNSS #execution #ltl #model checking

A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.

CAV-2012-EsparzaGK #probability #proving #source code #termination #using

Proving Termination of Probabilistic Programs Using Patterns (JE, AG, SK), pp. 123–138.

CAV-2012-KretinskyE #automaton #ltl

Deterministic Automata for the (F, G)-Fragment of LTL (JK, JE), pp. 7–22.

LICS-2012-EsparzaGM #bound #verification

A Perfect Model for Bounded Verification (JE, PG, RM), pp. 285–294.

POPL-2011-EsparzaG #complexity #parallel #source code #thread #verification

Complexity of pattern-based verification for multithreaded programs (JE, PG), pp. 499–510.

SAS-2011-EsparzaG #abstraction #probability

Probabilistic Abstractions with Arbitrary Domains (JE, AG), pp. 334–350.

ICALP-v2-2010-BrazdilEKL #scheduling

Space-Efficient Scheduling of Stochastically Generated Tasks (TB, JE, SK, ML), pp. 539–550.

ICGT-2010-Esparza #concurrent #tool support

A False History of True Concurrency: From Petri to Tools (JE), pp. 1–2.

ICGT-2010-KonigE #graph transformation #specification #verification

Verification of Graph Transformation Systems with Context-Free Specifications (BK, JE), pp. 107–122.

VMCAI-2010-Esparza #analysis #probability #process

Analysis of Systems with Stochastic Process Creation (JE), p. 1.

DLT-2008-EsparzaKL #analysis #fixpoint

Derivation Tree Analysis for Accelerated Fixed-Point Computation (JE, SK, ML), pp. 301–313.

ICALP-A-2008-EsparzaGKS #approximate #equation

Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations (JE, TG, SK, HS), pp. 698–710.

ICALP-B-2008-EsparzaKL

Newton’s Method for ω-Continuous Semirings (JE, SK, ML), pp. 14–26.

TACAS-2008-BouajjaniESS #named

SDSIrep: A Reputation System Based on SDSI (AB, JE, SS, DS), pp. 501–516.

CAV-2007-SuwimonteerabuthBSE #java #named #source code #testing

jMoped: A Test Environment for Java Programs (DS, FB, SS, JE), pp. 164–167.

DLT-2007-EsparzaKL

An Extension of Newton’s Method to ω-Continuous Semirings (JE, SK, ML), pp. 157–168.

STOC-2007-KieferLE #convergence #equation #on the #polynomial

On the convergence of Newton’s method for monotone systems of polynomial equations (SK, ML, JE), pp. 217–226.

RTA-2006-BouajjaniE #modelling #source code

Rewriting Models of Boolean Programs (AB, JE), pp. 136–150.

TACAS-2006-EsparzaKS #abstraction #automaton #refinement

Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems (JE, SK, SS), pp. 489–503.

LICS-2005-EsparzaKM #analysis #automaton #probability

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances (JE, AK, RM), pp. 117–126.

SAS-2005-EsparzaGS #abstraction

Locality-Based Abstractions (JE, PG, SS), pp. 118–134.

TACAS-2005-SchwoonE #algorithm #on the fly #verification

A Note on On-the-Fly Verification Algorithms (SS, JE), pp. 174–190.

TACAS-2005-SuwimonteerabuthSE #bytecode #java #named

jMoped: A Java Bytecode Checker Based on Moped (DS, SS, JE), pp. 541–545.

LICS-2004-EsparzaKM #automaton #model checking #probability

Model Checking Probabilistic Pushdown Automata (JE, AK, RM), pp. 12–21.

DLT-2003-Esparza #approach #verification

An Automata-Theoretic Approach to Software Verification (JE), p. 21.

POPL-2003-BouajjaniET #approach #concurrent #source code #static analysis

A generic approach to the static analysis of concurrent programs with procedures (AB, JE, TT), pp. 62–73.

TACAS-2003-EsparzaM #multi #protocol

Simple Representative Instantiations for Multicast Protocols (JE, MM), pp. 128–143.

SAS-2002-Esparza #algebra #approach #concurrent #static analysis

An Algebraic Approach to the Static Analysis of Concurrent Software (JE), p. 3.

CAV-2001-EsparzaS #model checking #recursion #source code

A BDD-Based Model Checker for Recursive Programs (JE, SS), pp. 324–336.

PPDP-2001-Esparza #declarative #model checking #source code

Model Checking (with) Declarative Programs (JE), p. 37.

CAV-2000-EsparzaHRS #algorithm #automaton #model checking #performance

Efficient Algorithms for Model Checking Pushdown Systems (JE, DH, PR, SS), pp. 232–247.

ICALP-2000-EsparzaH #approach #ltl #model checking

A New Unfolding Approach to LTL Model Checking (JE, KH), pp. 475–486.

POPL-2000-EsparzaP #algorithm #graph #interprocedural #parallel #performance

Efficient Algorithms for pre^* and post^* on Interprocedural Parallel Flow Graphs (JE, AP), pp. 1–11.

CSL-1999-DelzannoEP #analysis #constraints #protocol

Constraint-Based Analysis of Broadcast Protocols (GD, JE, AP), pp. 50–66.

CSL-1999-KuceraE #algebra #logic

A Logical Viewpoint on Process-Algebraic Quotients (AK, JE), pp. 499–514.

FoSSaCS-1999-EsparzaK #analysis #approach #data flow #interprocedural

An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis (JE, JK), pp. 14–30.

LICS-1999-EsparzaFM #on the #protocol #verification

On the Verification of Broadcast Protocols (JE, AF, RM), pp. 352–359.

ESOP-1996-MelzerE #integer #programming

Checking System Properties via Integer Programming (SM, JE), pp. 250–264.

ICALP-1996-BradfieldEM #calculus #effectiveness #linear #μ-calculus

An Effective Tableau System for the Linear Time μ-Calculus (JCB, JE, AM), pp. 98–109.

ICALP-1996-JancarE #bisimulation #petri net

Deciding Finiteness of Petri Nets Up To Bisimulation (PJ, JE), pp. 478–489.

TACAS-1996-EsparzaRV #algorithm

An Improvement of McMillan’s Unfolding Algorithm (JE, SR, WV), pp. 87–106.

CAV-1995-EsparzaK #branch #logic #model checking #on the #parallel #problem #process

On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes (JE, AK), pp. 353–366.

CSL-1991-BestE #model checking #persistent #petri net

Model Checking of Persistent Petri Nets (EB, JE), pp. 35–52.

TAPSOFT-1993-Esparza #model checking #using

Model Checking Using Net Unfoldings (JE), pp. 613–628.

FASE-2016-EsparzaH #reduction #workflow

Reduction Rules for Colored Workflow Nets (JE, PH), pp. 342–358.

CAV-2016-SickertEJK #automaton #linear #logic

Limit-Deterministic Büchi Automata for Linear Temporal Logic (SS, JE, SJ, JK), pp. 312–332.

CAV-2018-BlondinEJ #analysis #named #protocol

Peregrine: A Tool for the Analysis of Population Protocols (MB, JE, SJ), pp. 604–611.