Previous Work

Our previous work that the PaVeS research is build on:

Download full bibliography (as BibTex): Our previous work

2018

• Blondin, M., Esparza, J., Jaax, S.: Peregrine: A Tool for the Analysis of Population Protocols. In: Chockler, H. and Weissenbacher, G. (eds.) CAV (1). pp. 604-611. Springer (2018)
  populationproticols
  (test note)
  URL: Link

  Abstract BibTeX EndNote Download URL

  We introduce Peregrine, the first tool for the analysis and parameterized verification of population protocols. Population protocols are a model of computation very much studied by the distributed computing community, in which mobile anonymous agents interact stochastically to achieve a common task. Peregrine allows users to design protocols, to simulate them both manually and automatically, to gather statistics of properties such as convergence speed, and to verify correctness automatically. This paper describes the features of Peregrine and their implementation.

  

  
• Blondin, M., Esparza, J., Jaax, S., Kucera, A.: Black Ninjas in the Dark: Formal Analysis of Population Protocols. In: Dawar, A. and Grädel, E. (eds.) LICS. pp. 1-10. ACM (2018)
  populationproticols
  URL: Link

  Abstract BibTeX EndNote Download URL

  n this interactive paper, which you should preferably read con-nected to the Internet, the Black Ninjas introduce you to populationprotocols, a fundamental model of distributed computation, and torecent work by the authors and their colleagues on their automaticverification.

  

  

2017

• Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Inf. 54, 191-215 (2017)
  populationproticols verification

  BibTeX EndNote URL

  

  

2016

• Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Model Checking Population Protocols. In: Lal, A., Akshay, S., Saurabh, S., and Sen, S. (eds.) FSTTCS. pp. 27:1-27:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)
  ModelChecking PopulationProticols
  URL: Link

  BibTeX EndNote URL

  

  
• Esparza, J., Hoffmann, P., Saha, R.: Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets. CoRR. abs/1606.00175, (2016)
  Analysis

  BibTeX EndNote URL

  

  
• Esparza, J., Ganty, P., Majumdar, R.: Parameterized Verification of Asynchronous Shared-Memory Systems. J. ACM. 63, 10 (2016)
  Verification

  BibTeX EndNote URL

  

  

2015

• Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model Checking Parameterized Asynchronous Shared-Memory Systems. In: Kroening, D. and Pasareanu, C.S. (eds.) CAV (1). pp. 67-84. Springer (2015)
  modelchecking parametrized

  BibTeX EndNote URL

  

  

2014

• Esparza, J., Ganty, P., Poch, T.: Pattern-Based Verification for Multithreaded Programs. ACM Trans. Program. Lang. Syst. 36, 9:1-9:29 (2014)
  Verification

  BibTeX EndNote URL

  

  

2013

• Brázdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods in System Design. 43, 124-163 (2013)
  automata

  Abstract BibTeX EndNote URL

  The paper gives a summary of the existing results about algorithmic analysis of probabilistic pushdown automata and their subclasses.

  

  

2012

• Esparza, J., Gaiser, A., Kiefer, S.: Proving Termination of Probabilistic Programs Using Patterns. In: Madhusudan, P. and Seshia, S.A. (eds.) CAV. pp. 123-138. Springer (2012)
  termination

  BibTeX EndNote URL

  

  
• Brázdil, T., Esparza, J., Kiefer, S., Luttenberger, M.: Space-efficient scheduling of stochastically generated tasks. Inf. Comput. 210, 87-110 (2012)
  scheduling

  BibTeX EndNote URL