@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@inproceedings{HB-types2020,
address = {Turin, Italy},
year = 2021,
volume = {188},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Ugo de Liguoro and Stefano Berardi and Thorsten Altenkirch},
acronym = {{TYPES}'20},
booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {T}ypes for {P}roofs and {P}rograms
({TYPES}'20)},
author = {Gabriel Hondet and Fr{\'e}d{\'e}ric Blanqui},
title = {{Encoding of Predicate Subtyping with Proof Irrelevance in the $\Lambda \Pi$-Calculus Modulo Theory}},
pages = {6:1--6:18},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13885/},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13885/},
doi = {10.4230/LIPIcs.TYPES.2020.6}
}
@article{BCC-comp21,
publisher = {Springer},
journal = {Computing},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Optimized {SAT} encoding of conformance checking artefacts},
volume = {103},
number = {1},
pages = {29-50},
year = 2021,
doi = {10.1007/s00607-020-00831-8},
url = {https://doi.org/10.1007/s00607-020-00831-8}
}
@article{BCC-is21,
publisher = {Elsevier Science Publishers},
journal = {Information Systems},
author = {Mathilde Boltenhagen and Thomas Chatain and Josep Carmona},
title = {Anti-alignments—Measuring the precision of process models and event logs},
volume = {98},
year = 2021,
doi = {https://doi.org/10.1016/j.is.2020.101708},
url = {https://doi.org/10.1016/j.is.2020.101708},
note = {To appear}
}
@inproceedings{BDJKM-csl21,
address = {online},
month = may,
publisher = {{IEEE} Press},
editor = {Alina Oprea and Thorsten Holz},
acronym = {{S\&P}'21},
booktitle = {{P}roceedings of the 42nd IEEE Symposium on Security and Privacy
({S\&P}'21)},
author = {Baelde, David and Delaune, St{\'e}phanie and Jacomme, Charlie and
Koutsos, Adrien and Moreau, Sol{\`e}ne},
title = {An {I}nteractive {P}rover for {P}rotocol {V}erification in the {C}omputational {M}odel},
year = {2021},
pdf = {https://hal.archives-ouvertes.fr/hal-03172119},
url = {https://hal.archives-ouvertes.fr/hal-03172119},
note = {To appear}
}
@phdthesis{baelde-hdr2021,
author = {Baelde, David},
title = {Contributions to the {V}erification of {C}ryptographic {P}rotocols},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {M{\'e}moire d'habilitation},
year = 2021,
month = feb,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baelde-Hab2021.pdf},
url = {http://www.lsv.fr/~baelde/hdr/index.html}
}
@article{BLRPR-ic21,
author = {Bruy{\`e}re, V{\'e}ronique and Le Roux, St{\'e}phane and Pauly, Arno
and Raskin, Jean{-}Fran{\c{c}}ois},
title = {On the existence of weak subgame perfect equilibria},
volume = {276},
year = 2021,
doi = {https://doi.org/10.1016/j.ic.2020.104553},
url = {https://www.sciencedirect.com/science/article/pii/S0890540120300419?via%3Dihub}
}
@article{BBFLMR-fac21,
publisher = {Springer},
journal = {Formal Aspects of Computing},
author = {Bacci, Giovanni and
Bouyer, Patricia and
Fahrenberg, Uli and
Larsen, Kim and
Markey, Nicolas and
Reynier, Pierre{-}Alain},
title = {Optimal and robust controller synthesis using energy timed automata
with uncertainty},
volume = {33},
pages = {3--25},
year = 2021,
doi = {10.1007/s00165-020-00521-4},
url = {https://link.springer.com/article/10.1007/s00165-020-00521-4}
}
@article{DFM-jlc21,
publisher = {Oxford University Press},
journal = {Journal of Logic and Computation},
author = {Demri, St{\'e}phane and Fervari, Raul and Mansutti, Alessio},
title = {Internal proof calculi for modal logics with separating conjunction},
year = 2021,
note = {Accepted for publication to the Special issue of JLC on
External and Internal Calculi for Non Classical Logics.},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jlc21.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jlc21.pdf}
}
@article{DLM-jlc21,
publisher = {ACM Press},
journal = {ACM Transactions on Computational Logic},
author = {Demri, St{\'e}phane and {\'E}tienne Lozes and Mansutti, Alessio},
title = {The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic},
year = 2021,
note = {To appear},
url = {http://arxiv.org/abs/1810.05410},
pdf = {http://arxiv.org/abs/1810.05410}
}
@inproceedings{GH-stacs21,
address = {Saarbr{\"u}cken, Germany},
month = mar,
volume = {187},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Markus Bl{\"a}ser and Benjamin Monmege},
acronym = {{STACS}'21},
booktitle = {{P}roceedings of the 38th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'21)},
author = {G{\"o}ller, Stefan and Hilaire, Mathieu},
title = {{Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete}},
year = {2021},
doi = {10.4230/LIPIcs.STACS.2021.36},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13681/pdf/LIPIcs-STACS-2021-36.pdf},
url = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=13681}
}
@inproceedings{DM-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {Dinis, Bruno and Miquey, {\'E}tienne},
title = {Realizability with stateful computations for nonstandard analysis},
pages = {19:1-19:23},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.19},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13453/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13453/}
}
@inproceedings{Lopez-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {Aliaume Lopez},
title = {Preservation {T}heorems {T}hrough the {L}ens of {T}opology},
pages = {32:1-32:17},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.32},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13466/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13466/}
}
@inproceedings{Schnoebelen-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {{\relax Ph}ilippe Schnoebelen},
title = {On flat lossy channel machines},
pages = {37:1-37:22},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.37},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13471/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13471/}
}
@inproceedings{BRS-csl21,
address = {Ljubljana, Slovenia},
month = jan,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Baier, Christel and Goubault{-}Larrecq, Jean},
acronym = {{CSL}'21},
booktitle = {{P}roceedings of the 29th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'21)},
author = {Benedikt Bollig and Fedor Ryabinin and Arnaud Sangnier},
title = {Reachability in Distributed Memory Automata},
pages = {13:1-13:16},
year = {2021},
doi = {10.4230/LIPIcs.CSL.2021.13},
pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/},
url = {https://drops.dagstuhl.de/opus/volltexte/2021/13447/}
}
@techreport{DLM-arxiv20,
author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
institution = {Computing Research Repository},
month = feb,
note = {63~pages},
number = {2006.05156v2},
type = {Research Report},
title = {A {C}omplete {A}xiomatisation for {Q}uantifier-{F}ree {S}eparation {L}ogic},
year = {2021},
url = {https://arxiv.org/abs/2006.05156},
pdf = {https://arxiv.org/pdf/2006.05156v2.pdf}
}
@article{LRP-ic20,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Le Roux, St{\'e}phane and Pauly, Arno},
title = {Equilibria in multi-player multi-outcome infinite sequential games},
volume = {276},
year = 2021,
doi = {https://doi.org/10.1016/j.ic.2020.104557},
url = {https://www.sciencedirect.com/science/article/pii/S0890540120300456?via%3Dihub}
}
This file was generated by bibtex2html 1.98.