Previous Work

Our previous work that the PaVeS research is build on:

Download full bibliography (as BibTex): Our previous work

[2018] [2017] [2016] [2015] [2014] [2013] [2012]

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)
URL: Link
Keywords: conference

AbstractURLBibTeXEndNoteDownload

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.
@inproceedings{conf/cav/BlondinEJ18_noslides,
abstract = {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.},
author = {Blondin, Michael and Esparza, Javier and Jaax, Stefan},
booktitle = {CAV (1)},
crossref = {conf/cav/2018-1},
editor = {Chockler, Hana and Weissenbacher, Georg},
keywords = {conference},
pages = {604-611},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Peregrine: A Tool for the Analysis of Population Protocols.},
volume = 10981,
year = 2018
}
%0 Conference Paper
%1 conf/cav/BlondinEJ18_noslides
%A Blondin, Michael
%A Esparza, Javier
%A Jaax, Stefan
%B CAV (1)
%D 2018
%E Chockler, Hana
%E Weissenbacher, Georg
%I Springer
%P 604-611
%T Peregrine: A Tool for the Analysis of Population Protocols.
%U http://info.usherbrooke.ca/mblondin/papers/BEJ18b.pdf
%V 10981
%X 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.
%@ 978-3-319-96145-3
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)
URL: Link
Keywords: conference

AbstractURLBibTeXEndNoteDownload

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.
@inproceedings{conf/lics/BlondinEJK18,
abstract = {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.},
author = {Blondin, Michael and Esparza, Javier and Jaax, Stefan and Kucera, Antonín},
booktitle = {LICS},
crossref = {conf/lics/2018},
editor = {Dawar, Anuj and Grädel, Erich},
keywords = {conference},
pages = {1-10},
publisher = {ACM},
title = {Black Ninjas in the Dark: Formal Analysis of Population Protocols.},
year = 2018
}
%0 Conference Paper
%1 conf/lics/BlondinEJK18
%A Blondin, Michael
%A Esparza, Javier
%A Jaax, Stefan
%A Kucera, Antonín
%B LICS
%D 2018
%E Dawar, Anuj
%E Grädel, Erich
%I ACM
%P 1-10
%T Black Ninjas in the Dark: Formal Analysis of Population Protocols.
%U http://info.usherbrooke.ca/mblondin/papers/BEJK18.pdf
%X 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)
URL: Link
Keywords: journal

URLBibTeXEndNote

@article{journals/acta/EsparzaGLM17,
author = {Esparza, Javier and Ganty, Pierre and Leroux, Jérôme and Majumdar, Rupak},
journal = {Acta Inf.},
keywords = {journal},
number = 2,
pages = {191-215},
title = {Verification of population protocols.},
volume = 54,
year = 2017
}
%0 Journal Article
%1 journals/acta/EsparzaGLM17
%A Esparza, Javier
%A Ganty, Pierre
%A Leroux, Jérôme
%A Majumdar, Rupak
%D 2017
%J Acta Inf.
%N 2
%P 191-215
%R 10.1007/s00236-016-0272-3
%T Verification of population protocols.
%U https://doi.org/10.1007/s00236-016-0272-3
%V 54

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)
URL: Link
Keywords: conference

URLBibTeXEndNote

@inproceedings{conf/fsttcs/EsparzaGLM16,
author = {Esparza, Javier and Ganty, Pierre and Leroux, Jérôme and Majumdar, Rupak},
booktitle = {FSTTCS},
crossref = {conf/fsttcs/2016},
editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
keywords = {conference},
pages = {27:1-27:14},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
series = {LIPIcs},
title = {Model Checking Population Protocols.},
volume = 65,
year = 2016
}
%0 Conference Paper
%1 conf/fsttcs/EsparzaGLM16
%A Esparza, Javier
%A Ganty, Pierre
%A Leroux, Jérôme
%A Majumdar, Rupak
%B FSTTCS
%D 2016
%E Lal, Akash
%E Akshay, S.
%E Saurabh, Saket
%E Sen, Sandeep
%I Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
%P 27:1-27:14
%R 10.4230/LIPIcs.FSTTCS.2016.27
%T Model Checking Population Protocols.
%U http://drops.dagstuhl.de/opus/volltexte/2016/6862
%V 65
%@ 978-3-95977-027-9
Esparza, J., Hoffmann, P., Saha, R.: Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets. CoRR. abs/1606.00175, (2016)
URL: Link
Preprint: Link
Keywords: journal

URLBibTeXEndNote

@article{journals/corr/EsparzaHS16,
author = {Esparza, Javier and Hoffmann, Philipp and Saha, Ratul},
journal = {CoRR},
keywords = {journal},
note = {https://arxiv.org/abs/1606.00175},
title = {Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets.},
volume = {abs/1606.00175},
year = 2016
}
%0 Journal Article
%1 journals/corr/EsparzaHS16
%A Esparza, Javier
%A Hoffmann, Philipp
%A Saha, Ratul
%D 2016
%J CoRR
%R 10.1007/978-3-319-43425-4_6
%T Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets.
%U https://doi.org/10.1007/978-3-319-43425-4_6
%V abs/1606.00175
Esparza, J., Ganty, P., Majumdar, R.: Parameterized Verification of Asynchronous Shared-Memory Systems. J. ACM. 63, 10 (2016)
URL: Link
Keywords: journal

URLBibTeXEndNote

@article{journals/jacm/EsparzaGM16,
author = {Esparza, Javier and Ganty, Pierre and Majumdar, Rupak},
journal = {J. ACM},
keywords = {journal},
number = 1,
pages = 10,
title = {Parameterized Verification of Asynchronous Shared-Memory Systems.},
volume = 63,
year = 2016
}
%0 Journal Article
%1 journals/jacm/EsparzaGM16
%A Esparza, Javier
%A Ganty, Pierre
%A Majumdar, Rupak
%D 2016
%J J. ACM
%N 1
%P 10
%R 10.1145/2842603
%T Parameterized Verification of Asynchronous Shared-Memory Systems.
%U https://doi.org/10.1145/2842603
%V 63

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)
Keywords: conference

BibTeXEndNote

@inproceedings{conf/cav/Durand-Gasselin15,
author = {Durand-Gasselin, Antoine and Esparza, Javier and Ganty, Pierre and Majumdar, Rupak},
booktitle = {CAV (1)},
crossref = {conf/cav/2015-1},
editor = {Kroening, Daniel and Pasareanu, Corina S.},
keywords = {conference},
pages = {67-84},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Model Checking Parameterized Asynchronous Shared-Memory Systems.},
volume = 9206,
year = 2015
}
%0 Conference Paper
%1 conf/cav/Durand-Gasselin15
%A Durand-Gasselin, Antoine
%A Esparza, Javier
%A Ganty, Pierre
%A Majumdar, Rupak
%B CAV (1)
%D 2015
%E Kroening, Daniel
%E Pasareanu, Corina S.
%I Springer
%P 67-84
%T Model Checking Parameterized Asynchronous Shared-Memory Systems.
%V 9206
%@ 978-3-319-21689-8

2014

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

BibTeXEndNote

@article{journals/toplas/EsparzaGP14,
author = {Esparza, Javier and Ganty, Pierre and Poch, Tomás},
journal = {ACM Trans. Program. Lang. Syst.},
keywords = {journal},
number = 3,
pages = {9:1-9:29},
title = {Pattern-Based Verification for Multithreaded Programs.},
volume = 36,
year = 2014
}
%0 Journal Article
%1 journals/toplas/EsparzaGP14
%A Esparza, Javier
%A Ganty, Pierre
%A Poch, Tomás
%D 2014
%J ACM Trans. Program. Lang. Syst.
%N 3
%P 9:1-9:29
%R 10.1145/2629644
%T Pattern-Based Verification for Multithreaded Programs.
%V 36

2013

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

AbstractBibTeXEndNote

The paper gives a summary of the existing results about algorithmic analysis of probabilistic pushdown automata and their subclasses.
@article{journals/fmsd/BrazdilEKK13,
abstract = {The paper gives a summary of the existing results about algorithmic analysis of probabilistic pushdown automata and their subclasses.},
author = {Brázdil, Tomás and Esparza, Javier and Kiefer, Stefan and Kucera, Antonín},
journal = {Formal Methods in System Design},
keywords = {journal},
number = 2,
pages = {124-163},
title = {Analyzing probabilistic pushdown automata.},
volume = 43,
year = 2013
}
%0 Journal Article
%1 journals/fmsd/BrazdilEKK13
%A Brázdil, Tomás
%A Esparza, Javier
%A Kiefer, Stefan
%A Kucera, Antonín
%D 2013
%J Formal Methods in System Design
%N 2
%P 124-163
%R 10.1007/s10703-012-0166-0
%T Analyzing probabilistic pushdown automata.
%V 43
%X 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)
Keywords: conference

BibTeXEndNote

@inproceedings{conf/cav/EsparzaGK12,
author = {Esparza, Javier and Gaiser, Andreas and Kiefer, Stefan},
booktitle = {CAV},
crossref = {conf/cav/2012},
editor = {Madhusudan, P. and Seshia, Sanjit A.},
keywords = {conference},
pages = {123-138},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Proving Termination of Probabilistic Programs Using Patterns.},
volume = 7358,
year = 2012
}
%0 Conference Paper
%1 conf/cav/EsparzaGK12
%A Esparza, Javier
%A Gaiser, Andreas
%A Kiefer, Stefan
%B CAV
%D 2012
%E Madhusudan, P.
%E Seshia, Sanjit A.
%I Springer
%P 123-138
%R 10.1007/978-3-642-31424-7_14
%T Proving Termination of Probabilistic Programs Using Patterns.
%V 7358
%@ 978-3-642-31423-0
Brázdil, T., Esparza, J., Kiefer, S., Luttenberger, M.: Space-efficient scheduling of stochastically generated tasks. Inf. Comput. 210, 87–110 (2012)
Keywords: journal

BibTeXEndNote

@article{journals/iandc/BrazdilEKL12,
author = {Brázdil, Tomás and Esparza, Javier and Kiefer, Stefan and Luttenberger, Michael},
journal = {Inf. Comput.},
keywords = {journal},
pages = {87-110},
title = {Space-efficient scheduling of stochastically generated tasks.},
volume = 210,
year = 2012
}
%0 Journal Article
%1 journals/iandc/BrazdilEKL12
%A Brázdil, Tomás
%A Esparza, Javier
%A Kiefer, Stefan
%A Luttenberger, Michael
%D 2012
%J Inf. Comput.
%P 87-110
%R 10.1016/j.ic.2011.10.005
%T Space-efficient scheduling of stochastically generated tasks.
%V 210