@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{M-fsttcs18,
address = {Ahmedabad, India},
month = dec,
year = 2018,
volume = {122},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Sumit Ganguly and Paritosh Pandya},
acronym = {{FSTTCS}'18},
booktitle = {{P}roceedings of the 38th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'18)},
author = {Alessio Mansutti},
title = {Extending propositional separation logic for robustness properties},
pages = {42:1-42:23},
url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9941},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9941/pdf/LIPIcs-FSTTCS-2018-42.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2018.42},
abstract = {We study an extension of propositional separation logic that can specify robustness properties, such as acyclicity and garbage freedom, for automatic verification of stateful programs with singly-linked lists. We show that its satisfiability problem is PSpace-complete, whereas modest extensions of the logic are shown to be Tower-hard. As separating implication, reachability predicates (under some syntactical restrictions) and a unique quantified variable are allowed, this logic subsumes several PSpace-complete separation logics considered in previous works.}
}
@inproceedings{DLM-fossacs18,
address = {Thessaloniki, Greece},
month = apr,
year = 2018,
volume = {10803},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Baier, Christel and {Dal Lago}, Ugo},
acronym = {{FoSSaCS}'18},
booktitle = {{P}roceedings of the 21st {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'18)},
author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
title = {The Effects of Adding Reachability Predicates in Propositional Separation Logic},
pages = {476-493},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DLM-fossacs18.pdf}
}
@inproceedings{DLM-csl20,
address = {Barcelona, Spain},
month = jan,
year = 2020,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Fern{\'a}ndel, Maribel and Muscholl, Anca},
acronym = {{CSL}'20},
booktitle = {{P}roceedings of the 28th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'20)},
author = {St{\'e}phane Demri and {\'E}tienne Lozes and Alessio Mansutti},
title = {Internal Calculi for Separation Logics},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/11662/},
doi = {10.4230/LIPIcs.CSL.2020.19}
}
@inproceedings{DFM-jelia19,
address = {Rende, Italy},
month = jun,
year = 2019,
volume = 11468,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Calimeri, Francesco and Leone, Nicola and Manna, Marco},
acronym = {{JELIA}'19},
booktitle = {{P}roceedings of the 16th {E}uropean {C}onference on {L}ogics in
{A}rtificial {I}ntelligence ({JELIA}'19)},
author = {Demri, St{\'e}phane and Fervari, Raul and Mansutti, Alessio},
title = {Axiomatising logics with separating conjunctions and modalities},
pages = {692-708},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jelia19.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFM-jelia19.pdf},
doi = {10.1007/978-3-030-19570-0_45}
}
@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}
}
@phdthesis{Mansutti-phd2020,
author = {Mansutti, Alessio},
title = {{Reasoning with Separation Logics: Complexity, Expressive Power, Proof Systems}},
school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
type = {Th{\`e}se de doctorat},
year = 2020,
month = dec,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mansutti-phd20.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/mansutti-phd20.pdf}
}
@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}
}
@inproceedings{BDFM-lics20,
address = {Saarbrucken, Germany},
month = jul,
publisher = {{IEEE} Press},
editor = {Kobayashi, Naoki},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 35th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'20)},
author = {Bednarczyk, Bartosz and Demri, St{\'e}phane and Fervari, Ra{\'u}l and Mansutti, Alessio},
title = {Modal Logics with Composition on Finite Forests: Expressivity and Complexity},
pages = {167--180},
year = 2020,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BDFM-lics2020.pdf},
doi = {https://dl.acm.org/doi/10.1145/3373718.3394787}
}
@inproceedings{BDM-ijcai20,
month = jul,
publisher = {IJCAI organization},
editor = {Bessi{\`e}re, Christian},
acronym = {{IJCAI}'20},
booktitle = {{P}roceedings of the 29th {I}nternational {J}oint
{C}onference on {A}rtificial {I}ntelligence
({IJCAI}'20)},
author = {Bednarczyk, Bartosz and Demri, St{\'e}phane and Mansutti, Alessio},
title = {A Framework for Reasoning about Dynamic Axioms in Description Logics},
optpages = {},
year = 2020,
optpdf = {},
url = {https://www.ijcai.org/Proceedings/2020/233},
optdoi = {}
}
@inproceedings{Mansutti-fossacs20,
address = {Dublin, Ireland},
month = apr,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Barbara K{\"o}nig and Jean Goubault-Larrecq},
acronym = {{FoSSaCS}'20},
booktitle = {{P}roceedings of the 23rd {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'20)},
author = {Alessio Mansutti},
title = {An auxiliary logic on trees: on the {T}ower-hardness of
logics featuring reachability and submodel reasoning},
pages = {462--481},
doi = {10.1007/978-3-030-45231-5_24},
year = 2020
}
This file was generated by bibtex2html 1.98.