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

1.
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
URL: Link
#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 = {populationproticols},
note = {#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
1.
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
#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 = {populationproticols},
note = {#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

1.
Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Inf. 54, 191–215 (2017)
populationproticols verification
URL: Link
#journal

URLBibTeXEndNote

@article{journals/acta/EsparzaGLM17,
author = {Esparza, Javier and Ganty, Pierre and Leroux, Jérôme and Majumdar, Rupak},
journal = {Acta Inf.},
keywords = {populationproticols verification},
note = {#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

1.
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
#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 = {ModelChecking PopulationProticols},
note = {#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
1.
Esparza, J., Hoffmann, P., Saha, R.: Polynomial Analysis Algorithms for Free Choice Probabilistic Workflow Nets. CoRR. abs/1606.00175, (2016)
Analysis
URL: Link
Preprint: <a href="https://arxiv.org/abs/1606.00175">Link</a><br>#journal

URLBibTeXEndNote

@article{journals/corr/EsparzaHS16,
author = {Esparza, Javier and Hoffmann, Philipp and Saha, Ratul},
journal = {CoRR},
keywords = {Analysis},
note = {Preprint: Link
#journal},
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
1.
Esparza, J., Ganty, P., Majumdar, R.: Parameterized Verification of Asynchronous Shared-Memory Systems. J. ACM. 63, 10 (2016)
Verification
URL: Link
#journal

URLBibTeXEndNote

@article{journals/jacm/EsparzaGM16,
author = {Esparza, Javier and Ganty, Pierre and Majumdar, Rupak},
journal = {J. ACM},
keywords = {Verification},
note = {#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

1.
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
#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 = {modelchecking parametrized},
note = {#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

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

BibTeXEndNote

@article{journals/toplas/EsparzaGP14,
author = {Esparza, Javier and Ganty, Pierre and Poch, Tomás},
journal = {ACM Trans. Program. Lang. Syst.},
keywords = {Verification},
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

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

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 = {automata},
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

1.
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

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 = {termination},
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
1.
Brázdil, T., Esparza, J., Kiefer, S., Luttenberger, M.: Space-efficient scheduling of stochastically generated tasks. Inf. Comput. 210, 87–110 (2012)
scheduling

BibTeXEndNote

@article{journals/iandc/BrazdilEKL12,
author = {Brázdil, Tomás and Esparza, Javier and Kiefer, Stefan and Luttenberger, Michael},
journal = {Inf. Comput.},
keywords = {scheduling},
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