Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)
Stéphane Demri and Karin Quaas. Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 29:1-29:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{demri_et_al:LIPIcs.CONCUR.2023.29, author = {Demri, St\'{e}phane and Quaas, Karin}, title = {{Constraint Automata on Infinite Data Trees: from CTL(\mathbb{Z})/CTL^*(\mathbb{Z}) to Decision Procedures}}, booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)}, pages = {29:1--29:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-299-0}, ISSN = {1868-8969}, year = {2023}, volume = {279}, editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.29}, URN = {urn:nbn:de:0030-drops-190238}, doi = {10.4230/LIPIcs.CONCUR.2023.29}, annote = {Keywords: Constraints, Constraint Automata, Temporal Logics, Infinite Data Trees} }
Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 111:1-111:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{baumann_et_al:LIPIcs.ICALP.2020.111, author = {Baumann, Pascal and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg}, title = {{The Complexity of Bounded Context Switching with Dynamic Thread Creation}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {111:1--111:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.111}, URN = {urn:nbn:de:0030-drops-125187}, doi = {10.4230/LIPIcs.ICALP.2020.111}, annote = {Keywords: Dynamic thread creation, Bounded context switching, Asynchronous Programs, Safety verification, State reachability, Petri nets, Complexity, Succinctness, Counter Programs} }
Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Stéphane Demri, Etienne Lozes, and Alessio Mansutti. Internal Calculi for Separation Logics. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 19:1-19:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{demri_et_al:LIPIcs.CSL.2020.19, author = {Demri, St\'{e}phane and Lozes, Etienne and Mansutti, Alessio}, title = {{Internal Calculi for Separation Logics}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {19:1--19:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.19}, URN = {urn:nbn:de:0030-drops-116625}, doi = {10.4230/LIPIcs.CSL.2020.19}, annote = {Keywords: Separation logic, internal calculus, adjunct/quantifier elimination} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{wu_et_al:LIPIcs.ITP.2019.31, author = {Wu, Minchao and Gor\'{e}, Rajeev}, title = {{Verified Decision Procedures for Modal Logics}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {31:1--31:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.31}, URN = {urn:nbn:de:0030-drops-110866}, doi = {10.4230/LIPIcs.ITP.2019.31}, annote = {Keywords: Formal Methods, Interactive Theorem Proving, Modal Logic, Lean} }
Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)
Alain Finkel and M. Praveen. Verification of Flat FIFO Systems. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{finkel_et_al:LIPIcs.CONCUR.2019.12, author = {Finkel, Alain and Praveen, M.}, title = {{Verification of Flat FIFO Systems}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {12:1--12:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.12}, URN = {urn:nbn:de:0030-drops-109147}, doi = {10.4230/LIPIcs.CONCUR.2019.12}, annote = {Keywords: Infinite state systems, FIFO, counters, flat systems, reachability, termination, complexity} }
Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Jérôme Leroux. Petri Net Reachability Problem (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{leroux:LIPIcs.MFCS.2019.5, author = {Leroux, J\'{e}r\^{o}me}, title = {{Petri Net Reachability Problem}}, booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)}, pages = {5:1--5:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-117-7}, ISSN = {1868-8969}, year = {2019}, volume = {138}, editor = {Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.5}, URN = {urn:nbn:de:0030-drops-109493}, doi = {10.4230/LIPIcs.MFCS.2019.5}, annote = {Keywords: Petri net, Reachability problem, Formal verification, Concurrency} }
Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)
Stéphane Demri. On Temporal and Separation Logics (Invited Paper). In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 1:1-1:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{demri:LIPIcs.TIME.2018.1, author = {Demri, St\'{e}phane}, title = {{On Temporal and Separation Logics}}, booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)}, pages = {1:1--1:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-089-7}, ISSN = {1868-8969}, year = {2018}, volume = {120}, editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.1}, URN = {urn:nbn:de:0030-drops-97662}, doi = {10.4230/LIPIcs.TIME.2018.1}, annote = {Keywords: separation logics, temporal logics, expressive power} }
Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)
Stéphane Demri, Etienne Lozes, and Denis Lugiez. On Symbolic Heaps Modulo Permission Theories. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 25:1-25:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{demri_et_al:LIPIcs.FSTTCS.2017.25, author = {Demri, St\'{e}phane and Lozes, Etienne and Lugiez, Denis}, title = {{On Symbolic Heaps Modulo Permission Theories}}, booktitle = {37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)}, pages = {25:1--25:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-055-2}, ISSN = {1868-8969}, year = {2018}, volume = {93}, editor = {Lokam, Satya and Ramanujam, R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.25}, URN = {urn:nbn:de:0030-drops-83887}, doi = {10.4230/LIPIcs.FSTTCS.2017.25}, annote = {Keywords: separation logic, entailment, permission, reasoning modulo theories} }
Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Thomas Colcombet and Amaldev Manuel. Fragments of Fixpoint Logic on Data Words. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 98-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2015.98, author = {Colcombet, Thomas and Manuel, Amaldev}, title = {{Fragments of Fixpoint Logic on Data Words}}, booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)}, pages = {98--111}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-97-2}, ISSN = {1868-8969}, year = {2015}, volume = {45}, editor = {Harsha, Prahladh and Ramalingam, G.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.98}, URN = {urn:nbn:de:0030-drops-56289}, doi = {10.4230/LIPIcs.FSTTCS.2015.98}, annote = {Keywords: Data words, Data automata, Fixpoint logic} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Lorenzo Clemente and Slawomir Lasota. Reachability Analysis of First-order Definable Pushdown Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 244-259, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{clemente_et_al:LIPIcs.CSL.2015.244, author = {Clemente, Lorenzo and Lasota, Slawomir}, title = {{Reachability Analysis of First-order Definable Pushdown Systems}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {244--259}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.244}, URN = {urn:nbn:de:0030-drops-54185}, doi = {10.4230/LIPIcs.CSL.2015.244}, annote = {Keywords: automata theory, pushdown systems, sets with atoms, saturation technique} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Stefan Hetzl and Sebastian Zivota. Tree Grammars for the Elimination of Non-prenex Cuts. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 110-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hetzl_et_al:LIPIcs.CSL.2015.110, author = {Hetzl, Stefan and Zivota, Sebastian}, title = {{Tree Grammars for the Elimination of Non-prenex Cuts}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {110--127}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.110}, URN = {urn:nbn:de:0030-drops-54103}, doi = {10.4230/LIPIcs.CSL.2015.110}, annote = {Keywords: proof theory, cut-elimination, Herbrand's theorem, tree grammars} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Claudia Carapelle and Markus Lohrey. Temporal Logics with Local Constraints (Invited Talk). In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 2-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{carapelle_et_al:LIPIcs.CSL.2015.2, author = {Carapelle, Claudia and Lohrey, Markus}, title = {{Temporal Logics with Local Constraints}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {2--13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.2}, URN = {urn:nbn:de:0030-drops-54465}, doi = {10.4230/LIPIcs.CSL.2015.2}, annote = {Keywords: Temporal logics with constraints, concrete domains, LTL, CTL*, ECTL*} }
Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Malte Schwerhoff and Alexander J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 614-638, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{schwerhoff_et_al:LIPIcs.ECOOP.2015.614, author = {Schwerhoff, Malte and Summers, Alexander J.}, title = {{Lightweight Support for Magic Wands in an Automatic Verifier}}, booktitle = {29th European Conference on Object-Oriented Programming (ECOOP 2015)}, pages = {614--638}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-86-6}, ISSN = {1868-8969}, year = {2015}, volume = {37}, editor = {Boyland, John Tang}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.614}, URN = {urn:nbn:de:0030-drops-52408}, doi = {10.4230/LIPIcs.ECOOP.2015.614}, annote = {Keywords: Magic Wand, Software Verification, Automatic Verifiers, Separation Logic, Implicit Dynamic Frames} }
Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Johannes Waldmann. Matrix Interpretations on Polyhedral Domains. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 318-333, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{waldmann:LIPIcs.RTA.2015.318, author = {Waldmann, Johannes}, title = {{Matrix Interpretations on Polyhedral Domains}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {318--333}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.318}, URN = {urn:nbn:de:0030-drops-52059}, doi = {10.4230/LIPIcs.RTA.2015.318}, annote = {Keywords: termination of term rewriting, matrix interpretations, constraint programming, linear inequalities} }
Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{afshari_et_al:LIPIcs.TLCA.2015.1, author = {Afshari, Bahareh and Hetzl, Stefan and Leigh, Graham E.}, title = {{Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {1--16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.1}, URN = {urn:nbn:de:0030-drops-51516}, doi = {10.4230/LIPIcs.TLCA.2015.1}, annote = {Keywords: Classical logic, Context-free grammars, Cut elimination, First-order logic, Herbrand's theorem, Proof theory} }
Feedback for Dagstuhl Publishing