78 Search Results for "David, Nicolas"


Document
Isometric Path Complexity of Graphs

Authors: Dibyayan Chakraborty, Jérémie Chalopin, Florent Foucaud, and Yann Vaxès

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
A set S of isometric paths of a graph G is "v-rooted", where v is a vertex of G, if v is one of the end-vertices of all the isometric paths in S. The isometric path complexity of a graph G, denoted by ipco (G), is the minimum integer k such that there exists a vertex v ∈ V(G) satisfying the following property: the vertices of any isometric path P of G can be covered by k many v-rooted isometric paths. First, we provide an O(n² m)-time algorithm to compute the isometric path complexity of a graph with n vertices and m edges. Then we show that the isometric path complexity remains bounded for graphs in three seemingly unrelated graph classes, namely, hyperbolic graphs, (theta, prism, pyramid)-free graphs, and outerstring graphs. Hyperbolic graphs are extensively studied in Metric Graph Theory. The class of (theta, prism, pyramid)-free graphs are extensively studied in Structural Graph Theory, e.g. in the context of the Strong Perfect Graph Theorem. The class of outerstring graphs is studied in Geometric Graph Theory and Computational Geometry. Our results also show that the distance functions of these (structurally) different graph classes are more similar than previously thought. There is a direct algorithmic consequence of having small isometric path complexity. Specifically, using a result of Chakraborty et al. [ISAAC 2022], we show that if the isometric path complexity of a graph G is bounded by a constant k, then there exists a k-factor approximation algorithm for Isometric Path Cover, whose objective is to cover all vertices of a graph with a minimum number of isometric paths.

Cite as

Dibyayan Chakraborty, Jérémie Chalopin, Florent Foucaud, and Yann Vaxès. Isometric Path Complexity of Graphs. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 32:1-32:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.MFCS.2023.32,
  author =	{Chakraborty, Dibyayan and Chalopin, J\'{e}r\'{e}mie and Foucaud, Florent and Vax\`{e}s, Yann},
  title =	{{Isometric Path Complexity of Graphs}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.32},
  URN =		{urn:nbn:de:0030-drops-185666},
  doi =		{10.4230/LIPIcs.MFCS.2023.32},
  annote =	{Keywords: Shortest paths, Isometric path complexity, Hyperbolic graphs, Truemper Configurations, Outerstring graphs, Isometric Path Cover}
}
Document
Recontamination Helps a Lot to Hunt a Rabbit

Authors: Thomas Dissaux, Foivos Fioravantes, Harmender Gahlawat, and Nicolas Nisse

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
The Hunters and Rabbit game is played on a graph G where the Hunter player shoots at k vertices in every round while the Rabbit player occupies an unknown vertex and, if it is not shot, must move to a neighbouring vertex after each round. The Rabbit player wins if it can ensure that its position is never shot. The Hunter player wins otherwise. The hunter number h(G) of a graph G is the minimum integer k such that the Hunter player has a winning strategy (i.e., allowing him to win whatever be the strategy of the Rabbit player). This game has been studied in several graph classes, in particular in bipartite graphs (grids, trees, hypercubes...), but the computational complexity of computing h(G) remains open in general graphs and even in more restricted graph classes such as trees. To progress further in this study, we propose a notion of monotonicity (a well-studied and useful property in classical pursuit-evasion games such as Graph Searching games) for the Hunters and Rabbit game imposing that, roughly, a vertex that has already been shot "must not host the rabbit anymore". This allows us to obtain new results in various graph classes. More precisely, let the monotone hunter number mh(G) of a graph G be the minimum integer k such that the Hunter player has a monotone winning strategy. We show that pw(G) ≤ mh(G) ≤ pw(G)+1 for any graph G with pathwidth pw(G), which implies that computing mh(G), or even approximating mh(G) up to an additive constant, is NP-hard. Then, we show that mh(G) can be computed in polynomial time in split graphs, interval graphs, cographs and trees. These results go through structural characterisations which allow us to relate the monotone hunter number with the pathwidth in some of these graph classes. In all cases, this allows us to specify the hunter number or to show that there may be an arbitrary gap between h and mh, i.e., that monotonicity does not help. In particular, we show that, for every k ≥ 3, there exists a tree T with h(T) = 2 and mh(T) = k. We conclude by proving that computing h (resp., mh) is FPT parameterised by the minimum size of a vertex cover.

Cite as

Thomas Dissaux, Foivos Fioravantes, Harmender Gahlawat, and Nicolas Nisse. Recontamination Helps a Lot to Hunt a Rabbit. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 42:1-42:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{dissaux_et_al:LIPIcs.MFCS.2023.42,
  author =	{Dissaux, Thomas and Fioravantes, Foivos and Gahlawat, Harmender and Nisse, Nicolas},
  title =	{{Recontamination Helps a Lot to Hunt a Rabbit}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{42:1--42:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.42},
  URN =		{urn:nbn:de:0030-drops-185763},
  doi =		{10.4230/LIPIcs.MFCS.2023.42},
  annote =	{Keywords: Hunter and Rabbit, Monotonicity, Graph Searching}
}
Document
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Authors: Nicolas Waldburger

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.

Cite as

Nicolas Waldburger. Checking Presence Reachability Properties on Parameterized Shared-Memory Systems. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 88:1-88:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{waldburger:LIPIcs.MFCS.2023.88,
  author =	{Waldburger, Nicolas},
  title =	{{Checking Presence Reachability Properties on Parameterized Shared-Memory Systems}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{88:1--88:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.88},
  URN =		{urn:nbn:de:0030-drops-186225},
  doi =		{10.4230/LIPIcs.MFCS.2023.88},
  annote =	{Keywords: Verification, Parameterized models, Distributed algorithms}
}
Document
When Should You Wait Before Updating? - Toward a Robustness Refinement

Authors: Swan Dubois, Laurent Feuilloley, Franck Petit, and Mikaël Rabie

Published in: LIPIcs, Volume 257, 2nd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2023)


Abstract
Consider a dynamic network and a given distributed problem. At any point in time, there might exist several solutions that are equally good with respect to the problem specification, but that are different from an algorithmic perspective, because some could be easier to update than others when the network changes. In other words, one would prefer to have a solution that is more robust to topological changes in the network; and in this direction the best scenario would be that the solution remains correct despite the dynamic of the network. In [Arnaud Casteigts et al., 2020], the authors introduced a very strong robustness criterion: they required that for any removal of edges that maintain the network connected, the solution remains valid. They focus on the maximal independent set problem, and their approach consists in characterizing the graphs in which there exists a robust solution (the existential problem), or even stronger, where any solution is robust (the universal problem). As the robustness criteria is very demanding, few graphs have a robust solution, and even fewer are such that all of their solutions are robust. In this paper, we ask the following question: Can we have robustness for a larger class of networks, if we bound the number k of edge removals allowed? To answer this question, we consider three classic problems: maximal independent set, minimal dominating set and maximal matching. For the universal problem, the answers for the three cases are surprisingly different. For minimal dominating set, the class does not depend on the number of edges removed. For maximal matching, removing only one edge defines a robust class related to perfect matchings, but for all other bounds k, the class is the same as for an arbitrary number of edge removals. Finally, for maximal independent set, there is a strict hierarchy of classes: the class for the bound k is strictly larger than the class for bound k+1. For the robustness notion of [Arnaud Casteigts et al., 2020], no characterization of the class for the existential problem is known, only a polynomial-time recognition algorithm. We show that the situation is even worse for bounded k: even for k = 1, it is NP-hard to decide whether a graph has a robust maximal independent set.

Cite as

Swan Dubois, Laurent Feuilloley, Franck Petit, and Mikaël Rabie. When Should You Wait Before Updating? - Toward a Robustness Refinement. In 2nd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 257, pp. 7:1-7:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{dubois_et_al:LIPIcs.SAND.2023.7,
  author =	{Dubois, Swan and Feuilloley, Laurent and Petit, Franck and Rabie, Mika\"{e}l},
  title =	{{When Should You Wait Before Updating? - Toward a Robustness Refinement}},
  booktitle =	{2nd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2023)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-275-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{257},
  editor =	{Doty, David and Spirakis, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2023.7},
  URN =		{urn:nbn:de:0030-drops-179435},
  doi =		{10.4230/LIPIcs.SAND.2023.7},
  annote =	{Keywords: Robustness, dynamic network, temporal graphs, edge removal, connectivity, footprint, packing/covering problems, maximal independent set, maximal matching, minimum dominating set, perfect matching, NP-hardness}
}
Document
Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling (Dagstuhl Seminar 22382)

Authors: Philipp Berens, Kyle Cranmer, Neil D. Lawrence, Ulrike von Luxburg, and Jessica Montgomery

Published in: Dagstuhl Reports, Volume 12, Issue 9 (2023)


Abstract
This report documents the programme and the outcomes of Dagstuhl Seminar 22382 "Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling". Today’s scientific challenges are characterised by complexity. Interconnected natural, technological, and human systems are influenced by forces acting across time- and spatial-scales, resulting in complex interactions and emergent behaviours. Understanding these phenomena - and leveraging scientific advances to deliver innovative solutions to improve society’s health, wealth, and well-being - requires new ways of analysing complex systems. The transformative potential of AI stems from its widespread applicability across disciplines, and will only be achieved through integration across research domains. AI for science is a rendezvous point. It brings together expertise from AI and application domains; combines modelling knowledge with engineering know-how; and relies on collaboration across disciplines and between humans and machines. Alongside technical advances, the next wave of progress in the field will come from building a community of machine learning researchers, domain experts, citizen scientists, and engineers working together to design and deploy effective AI tools. This report summarises the discussions from the seminar and provides a roadmap to suggest how different communities can collaborate to deliver a new wave of progress in AI and its application for scientific discovery.

Cite as

Philipp Berens, Kyle Cranmer, Neil D. Lawrence, Ulrike von Luxburg, and Jessica Montgomery. Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling (Dagstuhl Seminar 22382). In Dagstuhl Reports, Volume 12, Issue 9, pp. 150-199, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Article{berens_et_al:DagRep.12.9.150,
  author =	{Berens, Philipp and Cranmer, Kyle and Lawrence, Neil D. and von Luxburg, Ulrike and Montgomery, Jessica},
  title =	{{Machine Learning for Science: Bridging Data-Driven and Mechanistic Modelling (Dagstuhl Seminar 22382)}},
  pages =	{150--199},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{9},
  editor =	{Berens, Philipp and Cranmer, Kyle and Lawrence, Neil D. and von Luxburg, Ulrike and Montgomery, Jessica},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.9.150},
  URN =		{urn:nbn:de:0030-drops-178125},
  doi =		{10.4230/DagRep.12.9.150},
  annote =	{Keywords: machine learning, artificial intelligence, life sciences, physical sciences, environmental sciences, simulation, causality, modelling}
}
Document
Track A: Algorithms, Complexity and Games
Threshold Rates of Code Ensembles: Linear Is Best

Authors: Nicolas Resch and Chen Yuan

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
In this work, we prove new results concerning the combinatorial properties of random linear codes. By applying the thresholds framework from Mosheiff et al. (FOCS 2020) we derive fine-grained results concerning the list-decodability and -recoverability of random linear codes. Firstly, we prove a lower bound on the list-size required for random linear codes over 𝔽_q ε-close to capacity to list-recover with error radius ρ and input lists of size 𝓁. We show that the list-size L must be at least {log_q binom{q,𝓁}}-R}/ε, where R is the rate of the random linear code. This is analogous to a lower bound for list-decoding that was recently obtained by Guruswami et al. (IEEE TIT 2021B). As a comparison, we also pin down the list size of random codes which is {log_q binom{q,𝓁}}/ε. This result almost closes the O({q log L}/L) gap left by Guruswami et al. (IEEE TIT 2021A). This leaves open the possibility (that we consider likely) that random linear codes perform better than the random codes for list-recoverability, which is in contrast to a recent gap shown for the case of list-recovery from erasures (Guruswami et al., IEEE TIT 2021B). Next, we consider list-decoding with constant list-sizes. Specifically, we obtain new lower bounds on the rate required for: - List-of-3 decodability of random linear codes over 𝔽₂; - List-of-2 decodability of random linear codes over 𝔽_q (for any q). This expands upon Guruswami et al. (IEEE TIT 2021A) which only studied list-of-2 decodability of random linear codes over 𝔽₂. Further, in both cases we are able to show that the rate is larger than that which is possible for uniformly random codes. A conclusion that we draw from our work is that, for many combinatorial properties of interest, random linear codes actually perform better than uniformly random codes, in contrast to the apparently standard intuition that uniformly random codes are best.

Cite as

Nicolas Resch and Chen Yuan. Threshold Rates of Code Ensembles: Linear Is Best. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 104:1-104:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{resch_et_al:LIPIcs.ICALP.2022.104,
  author =	{Resch, Nicolas and Yuan, Chen},
  title =	{{Threshold Rates of Code Ensembles: Linear Is Best}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{104:1--104:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.104},
  URN =		{urn:nbn:de:0030-drops-164456},
  doi =		{10.4230/LIPIcs.ICALP.2022.104},
  annote =	{Keywords: Random Linear Codes, List-Decoding, List-Recovery, Threshold Rates}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Parameterized Safety Verification of Round-Based Shared-Memory Systems

Authors: Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [James Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

Cite as

Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized Safety Verification of Round-Based Shared-Memory Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 113:1-113:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.ICALP.2022.113,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sankur, Ocan and Waldburger, Nicolas},
  title =	{{Parameterized Safety Verification of Round-Based Shared-Memory Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{113:1--113:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.113},
  URN =		{urn:nbn:de:0030-drops-164541},
  doi =		{10.4230/LIPIcs.ICALP.2022.113},
  annote =	{Keywords: Verification, Parameterized models, Distributed algorithms}
}
Document
Framing Algorithms for Approximate Multicriteria Shortest Paths

Authors: Nicolas Hanusse, David Ilcinkas, and Antonin Lentz

Published in: OASIcs, Volume 85, 20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020)


Abstract
This paper deals with the computation of d-dimensional multicriteria shortest paths. In a weighted graph with arc weights represented by vectors, the cost of a path is the vector sum of the weights of its arcs. For a given pair consisting of a source s and a destination t, a path P dominates a path Q if and only if P’s cost is component-wise smaller than or equal to Q’s cost. The set of Pareto paths, or Pareto set, from s to t is the set of paths that are not dominated. The computation time of the Pareto paths can be prohibitive whenever the set of Pareto paths is large. We propose in this article new algorithms to compute approximated Pareto paths in any dimension. For d = 2, we exhibit the first approximation algorithm, called Frame, whose output is guaranteed to be always a subset of the Pareto set. Finally, we provide a small experimental study in order to confirm the relevance of our Frame algorithm.

Cite as

Nicolas Hanusse, David Ilcinkas, and Antonin Lentz. Framing Algorithms for Approximate Multicriteria Shortest Paths. In 20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020). Open Access Series in Informatics (OASIcs), Volume 85, pp. 11:1-11:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{hanusse_et_al:OASIcs.ATMOS.2020.11,
  author =	{Hanusse, Nicolas and Ilcinkas, David and Lentz, Antonin},
  title =	{{Framing Algorithms for Approximate Multicriteria Shortest Paths}},
  booktitle =	{20th Symposium on Algorithmic Approaches for Transportation Modelling, Optimization, and Systems (ATMOS 2020)},
  pages =	{11:1--11:19},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-170-2},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{85},
  editor =	{Huisman, Dennis and Zaroliagis, Christos D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2020.11},
  URN =		{urn:nbn:de:0030-drops-131476},
  doi =		{10.4230/OASIcs.ATMOS.2020.11},
  annote =	{Keywords: Pareto set, multicriteria, shortest paths, approximation}
}
Document
Artifact
Multiparty Session Programming with Global Protocol Combinators (Artifact)

Authors: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
In the paper "Multiparty Session Programming with Global Protocol Combinators", we introduce a library, ocaml-mpst for programming with global combinators - a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. This artifact is the source code of ocaml-mpst, with all the examples and benchmarks discussed in the paper.

Cite as

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming with Global Protocol Combinators (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Article{imai_et_al:DARTS.6.2.18,
  author =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  title =	{{Multiparty Session Programming with Global Protocol Combinators (Artifact)}},
  pages =	{18:1--18:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Imai, Keigo and Neykova, Rumyana and Yoshida, Nobuko and Yuen, Shoji},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.18},
  URN =		{urn:nbn:de:0030-drops-132159},
  doi =		{10.4230/DARTS.6.2.18},
  annote =	{Keywords: Multiparty Session Types, Communication Protocol, Concurrent and Distributed Programming, OCaml}
}
Document
Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model

Authors: Sam Van den Vonder, Thierry Renaux, Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
Reactive programming is a programming paradigm whereby programs are internally represented by a dependency graph, which is used to automatically (re)compute parts of a program whenever its input changes. In practice reactive programming can only be used for some parts of an application: a reactive program is usually embedded in an application that is still written in ordinary imperative languages such as JavaScript or Scala. In this paper we investigate this embedding and we distill "the awkward squad for reactive programming" as 3 concerns that are essential for real-world software development, but that do not fit within reactive programming. They are related to long lasting computations, side-effects, and the coordination between imperative and reactive code. To solve these issues we design a new programming model called the Actor-Reactor Model in which programs are split up in a number of actors and reactors. Actors and reactors enforce a strict separation of imperative and reactive code, and they can be composed via a number of composition operators that make use of data streams. We demonstrate the model via our own implementation in a language called Stella.

Cite as

Sam Van den Vonder, Thierry Renaux, Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter. Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 19:1-19:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{vandenvonder_et_al:LIPIcs.ECOOP.2020.19,
  author =	{Van den Vonder, Sam and Renaux, Thierry and Oeyen, Bjarno and De Koster, Joeri and De Meuter, Wolfgang},
  title =	{{Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{19:1--19:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.19},
  URN =		{urn:nbn:de:0030-drops-131768},
  doi =		{10.4230/LIPIcs.ECOOP.2020.19},
  annote =	{Keywords: functional reactive programming, reactive programming, reactive streams, actors, reactors}
}
Document
Space and Time Trade-Off for the k Shortest Simple Paths Problem

Authors: Ali Al Zoobi, David Coudert, and Nicolas Nisse

Published in: LIPIcs, Volume 160, 18th International Symposium on Experimental Algorithms (SEA 2020)


Abstract
The k shortest simple path problem (kSSP) asks to compute a set of top-k shortest simple paths from a vertex s to a vertex t in a digraph. Yen (1971) proposed the first algorithm with the best known theoretical complexity of O(kn(m+n log n)) for a digraph with n vertices and m arcs. Since then, the problem has been widely studied from an algorithm engineering perspective, and impressive improvements have been achieved. In particular, Kurz and Mutzel (2016) proposed a sidetracks-based (SB) algorithm which is currently the fastest solution. In this work, we propose two improvements of this algorithm. We first show how to speed up the SB algorithm using dynamic updates of shortest path trees. We did experiments on some road networks of the 9th DIMAC'S challenge with up to about half a million nodes and one million arcs. Our computational results show an average speed up by a factor of 1.5 to 2 with a similar working memory consumption as SB. We then propose a second algorithm enabling to significantly reduce the working memory at the cost of an increase of the running time (up to two times slower). Our experiments on the same data set show, on average, a reduction by a factor of 1.5 to 2 of the working memory.

Cite as

Ali Al Zoobi, David Coudert, and Nicolas Nisse. Space and Time Trade-Off for the k Shortest Simple Paths Problem. In 18th International Symposium on Experimental Algorithms (SEA 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 160, pp. 18:1-18:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{alzoobi_et_al:LIPIcs.SEA.2020.18,
  author =	{Al Zoobi, Ali and Coudert, David and Nisse, Nicolas},
  title =	{{Space and Time Trade-Off for the k Shortest Simple Paths Problem}},
  booktitle =	{18th International Symposium on Experimental Algorithms (SEA 2020)},
  pages =	{18:1--18:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-148-1},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{160},
  editor =	{Faro, Simone and Cantone, Domenico},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2020.18},
  URN =		{urn:nbn:de:0030-drops-120925},
  doi =		{10.4230/LIPIcs.SEA.2020.18},
  annote =	{Keywords: k shortest simple paths, graph algorithm, space-time trade-off}
}
Document
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq

Authors: Enrico Tassi

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We describe a procedure to derive equality tests and their correctness proofs from inductive type declarations in Coq. Programs and proofs are derived compositionally, reusing code and proofs derived previously. The key steps are two. First, we design appropriate induction principles for data types defined using parametric containers. Second, we develop a technique to work around the modularity limitations imposed by the purely syntactic termination check Coq performs on recursive proofs. The unary parametricity translation of inductive data types turns out to be the key to both steps. Last but not least, we provide an implementation of the procedure for the Coq proof assistant based on the Elpi [Dunchev et al., 2015] extension language.

Cite as

Enrico Tassi. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{tassi:LIPIcs.ITP.2019.29,
  author =	{Tassi, Enrico},
  title =	{{Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{29:1--29:18},
  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.29},
  URN =		{urn:nbn:de:0030-drops-110841},
  doi =		{10.4230/LIPIcs.ITP.2019.29},
  annote =	{Keywords: Coq, Containers, Induction, Equality test, Parametricity translation}
}
Document
A Certificate-Based Approach to Formally Verified Approximations

Authors: Florent Bréhard, Assia Mahboubi, and Damien Pous

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.

Cite as

Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{brehard_et_al:LIPIcs.ITP.2019.8,
  author =	{Br\'{e}hard, Florent and Mahboubi, Assia and Pous, Damien},
  title =	{{A Certificate-Based Approach to Formally Verified Approximations}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{8:1--8: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.8},
  URN =		{urn:nbn:de:0030-drops-110638},
  doi =		{10.4230/LIPIcs.ITP.2019.8},
  annote =	{Keywords: approximation theory, Chebyshev polynomials, Banach fixed-point theorem, interval arithmetic, Coq}
}
Document
Ornaments for Proof Reuse in Coq

Authors: Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.

Cite as

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{ringer_et_al:LIPIcs.ITP.2019.26,
  author =	{Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan},
  title =	{{Ornaments for Proof Reuse in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{26:1--26: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.26},
  URN =		{urn:nbn:de:0030-drops-110816},
  doi =		{10.4230/LIPIcs.ITP.2019.26},
  annote =	{Keywords: ornaments, proof reuse, proof automation}
}
Document
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Authors: Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized asymptotic complexity of the modified algorithm.

Cite as

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gueneau_et_al:LIPIcs.ITP.2019.18,
  author =	{Gu\'{e}neau, Arma\"{e}l and Jourdan, Jacques-Henri and Chargu\'{e}raud, Arthur and Pottier, Fran\c{c}ois},
  title =	{{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{18:1--18:20},
  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.18},
  URN =		{urn:nbn:de:0030-drops-110739},
  doi =		{10.4230/LIPIcs.ITP.2019.18},
  annote =	{Keywords: interactive deductive program verification, complexity analysis}
}
  • Refine by Author
  • 5 Markey, Nicolas
  • 2 Bouyer, Patricia
  • 2 Brihaye, Thomas
  • 2 Bruyère, Véronique
  • 2 David, Nicolas
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Design and analysis of algorithms
  • 3 Theory of computation → Distributed algorithms
  • 3 Theory of computation → Verification by model checking
  • 2 Mathematics of computing → Discrete mathematics
  • 2 Mathematics of computing → Graph algorithms
  • Show More...

  • Refine by Keyword
  • 3 Verification
  • 3 approximation
  • 2 Coq
  • 2 Coverability
  • 2 Distributed algorithms
  • Show More...

  • Refine by Type
  • 78 document

  • Refine by Publication Year
  • 34 2015
  • 22 2019
  • 7 2014
  • 5 2023
  • 4 2020
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail