8 Search Results for "Nicolas, Pascal"

Document
DOI: 10.4230/LIPIcs.ITP.2022.25
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant

Authors: Nicolas Magaud

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We formally implement the smallest three-dimensional projective space PG(3,2) in the Coq proof assistant. This projective space features 15 points and 35 lines, related by an incidence relation. We define points and lines as two plain datatypes (one with 15 constructors for points, and one with 35 constructors for lines) and the incidence relation as a boolean function, instead of using the well-known coordinate-based approach relying on GF(2)⁴. We prove that this implementation actually verifies all the usual properties of three-dimensional projective spaces. We then use an oracle to compute some characteristic subsets of objects of PG(3,2), namely spreads and packings. We formally verify that these computed objects exactly correspond to the spreads and packings of PG(3,2). For spreads, this means identifying 56 specific sets of 5 lines among 360 360 (= 15× 14× 13× 12× 11) possible ones. We then classify them, showing that the 56 spreads of PG(3,2) are all isomorphic whereas the 240 packings of PG(3,2) can be classified into two distinct classes of 120 elements. Proving these results requires partially automating the generation of some large specification files as well as some even larger proof scripts. Overall, this work can be viewed as an example of a large-scale combination of interactive and automated specifications and proofs. It is also a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).
Cite as

Nicolas Magaud. Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{magaud:LIPIcs.ITP.2022.25,
  author =	{Magaud, Nicolas},
  title =	{{Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.25},
  URN =		{urn:nbn:de:0030-drops-167349},
  doi =		{10.4230/LIPIcs.ITP.2022.25},
  annote =	{Keywords: Coq, projective geometry, finite models, spreads, packings, PG(3, 2)}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2019.14
A Generic Undo Support for State-Based CRDTs

Authors: Weihai Yu, Victorien Elvinger, and Claudia-Lavinia Ignat

Published in: LIPIcs, Volume 153, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019)

Abstract
CRDTs (Conflict-free Replicated Data Types) have properties desirable for large-scale distributed systems with variable network latency or transient partitions. With CRDT, data are always available for local updates and data states converge when the replicas have incorporated the same updates. Undo is useful for correcting human mistakes and for restoring system-wide invariant violated due to long delays or network partitions. There is currently no generally applicable undo support for CRDTs. There are at least two reasons for this. First, there is currently no abstraction that we can practically use to capture the relations between undo and normal operations with respect to concurrency and causality. Second, using inverse operations as the existing partial solutions, the CRDT designer has to hard-code certain rules and design a new CRDT for almost every operation that needs undo support. In this paper, we present an approach to generic support of undo for CRDTs. The approach consists of two major parts. We first work out an abstraction that captures the semantics of concurrent undo and redo operations through equivalence classes. The abstraction is a natural extension of undo and redo in sequential applications and is straightforward to implement in practice. By using this abstraction, we then device a mechanism to augment existing CRDTs. The mechanism provides an "out of the box" support for undo without the involvement of the CRDT designers. We also present a practical application of the approach in collaborative editing.
Cite as

Weihai Yu, Victorien Elvinger, and Claudia-Lavinia Ignat. A Generic Undo Support for State-Based CRDTs. In 23rd International Conference on Principles of Distributed Systems (OPODIS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 153, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{yu_et_al:LIPIcs.OPODIS.2019.14,
  author =	{Yu, Weihai and Elvinger, Victorien and Ignat, Claudia-Lavinia},
  title =	{{A Generic Undo Support for State-Based CRDTs}},
  booktitle =	{23rd International Conference on Principles of Distributed Systems (OPODIS 2019)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-133-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{153},
  editor =	{Felber, Pascal and Friedman, Roy and Gilbert, Seth and Miller, Avery},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2019.14},
  URN =		{urn:nbn:de:0030-drops-118009},
  doi =		{10.4230/LIPIcs.OPODIS.2019.14},
  annote =	{Keywords: Data replication, eventual consistency, state-based CRDT, delta-state CRDT, concurrent undo}
}
Document
DOI: 10.4230/LITES-v006-i001-a002
Improving WCET Evaluation using Linear Relation Analysis

Authors: Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet

Published in: LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1

Abstract
The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.
Cite as

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet. Improving WCET Evaluation using Linear Relation Analysis. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 02:1-02:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{raymond_et_al:LITES-v006-i001-a002,
  author =	{Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, R\'{e}my},
  title =	{{Improving WCET Evaluation using Linear Relation Analysis}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{02:1--02:28},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a002},
  doi =		{10.4230/LITES-v006-i001-a002},
  annote =	{Keywords: Worst Case Execution Time estimation, Infeasible Execution Paths, Abstract Interpretation}
}
Document
DOI: 10.4230/OASIcs.WCET.2017.9
The W-SEPT Project: Towards Semantic-Aware WCET Estimation

Authors: Claire Maiza, Pascal Raymond, Catherine Parent-Vigouroux, Armelle Bonenfant, Fabienne Carrier, Hugues Cassé, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Erwan Jahier, Hanbing Li, Marianne de Michiel, Vincent Mussot, Isabelle Puaut, Christine Rochange, Erven Rohou, Jordy Ruiz, Pascal Sotin, and Wei-Tsun Sun

Published in: OASIcs, Volume 57, 17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017)

Abstract
Critical embedded systems are generally composed of repetitive tasks that must meet hard timing constraints, such as termination deadlines. Providing an upper bound of the worst-case execution time (WCET) of such tasks at design time is necessary to guarantee the correctness of the system. In static WCET analysis, a main source of over-approximation comes from the complexity of the modern hardware platforms: their timing behavior tends to become more unpredictable because of features like caches, pipeline, branch prediction, etc. Another source of over-approximation comes from the software itself: WCET analysis may consider potential worst-cases executions that are actually infeasible, because of the semantics of the program or because they correspond to unrealistic inputs. The W-SEPT project, for "WCET, Semantics, Precision and Traceability", has been carried out to study and exploit the influence of program semantics on the WCET estimation. This paper presents the results of this project : a semantic-aware WCET estimation workflow for high-level designed systems.
Cite as

Claire Maiza, Pascal Raymond, Catherine Parent-Vigouroux, Armelle Bonenfant, Fabienne Carrier, Hugues Cassé, Philippe Cuenot, Denis Claraz, Nicolas Halbwachs, Erwan Jahier, Hanbing Li, Marianne de Michiel, Vincent Mussot, Isabelle Puaut, Christine Rochange, Erven Rohou, Jordy Ruiz, Pascal Sotin, and Wei-Tsun Sun. The W-SEPT Project: Towards Semantic-Aware WCET Estimation. In 17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017). Open Access Series in Informatics (OASIcs), Volume 57, pp. 9:1-9:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{maiza_et_al:OASIcs.WCET.2017.9,
  author =	{Maiza, Claire and Raymond, Pascal and Parent-Vigouroux, Catherine and Bonenfant, Armelle and Carrier, Fabienne and Cass\'{e}, Hugues and Cuenot, Philippe and Claraz, Denis and Halbwachs, Nicolas and Jahier, Erwan and Li, Hanbing and de Michiel, Marianne and Mussot, Vincent and Puaut, Isabelle and Rochange, Christine and Rohou, Erven and Ruiz, Jordy and Sotin, Pascal and Sun, Wei-Tsun},
  title =	{{The W-SEPT Project: Towards Semantic-Aware WCET Estimation}},
  booktitle =	{17th International Workshop on Worst-Case Execution Time Analysis (WCET 2017)},
  pages =	{9:1--9:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-057-6},
  ISSN =	{2190-6807},
  year =	{2017},
  volume =	{57},
  editor =	{Reineke, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2017.9},
  URN =		{urn:nbn:de:0030-drops-73097},
  doi =		{10.4230/OASIcs.WCET.2017.9},
  annote =	{Keywords: Worst-case execution time analysis, Static analysis, Program analysis}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.32
Canonizing Graphs of Bounded Tree Width in Logspace

Authors: Michael Elberfeld and Pascal Schweitzer

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
Graph canonization is the problem of computing a unique representative, a canon, from the isomorphism class of a given graph. This implies that two graphs are isomorphic exactly if their canons are equal. We show that graphs of bounded tree width can be canonized in deterministic logarithmic space (logspace). This implies that the isomorphism problem for graphs of bounded tree width can be decided in logspace. In the light of isomorphism for trees being hard for the complexity class logspace, this makes the ubiquitous classes of graphs of bounded tree width one of the few classes of graphs for which the complexity of the isomorphism problem has been exactly determined.
Cite as

Michael Elberfeld and Pascal Schweitzer. Canonizing Graphs of Bounded Tree Width in Logspace. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{elberfeld_et_al:LIPIcs.STACS.2016.32,
  author =	{Elberfeld, Michael and Schweitzer, Pascal},
  title =	{{Canonizing Graphs of Bounded Tree Width in Logspace}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.32},
  URN =		{urn:nbn:de:0030-drops-57336},
  doi =		{10.4230/LIPIcs.STACS.2016.32},
  annote =	{Keywords: algorithmic graph theory, computational complexity, graph isomorphism, logspace, tree width}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.689
Towards an Isomorphism Dichotomy for Hereditary Graph Classes

Authors: Pascal Schweitzer

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
In this paper we resolve the complexity of the isomorphism problem on all but finitely many of the graph classes characterized by two forbidden induced subgraphs. To this end we develop new techniques applicable for the structural and algorithmic analysis of graphs. First, we develop a methodology to show isomorphism completeness of the isomorphism problem on graph classes by providing a general framework unifying various reduction techniques. Second, we generalize the concept of the modular decomposition to colored graphs, allowing for non-standard decompositions. We show that, given a suitable decomposition functor, the graph isomorphism problem reduces to checking isomorphism of colored prime graphs. Third, we extend the techniques of bounded color valence and hypergraph isomorphism on hypergraphs of bounded color class size as follows. We say a colored graph has generalized color valence at most k if, after removing all vertices in color classes of size at most k, for each color class C every vertex has at most k neighbors in C or at most k non-neighbors in C. We show that isomorphism of graphs of bounded generalized color valence can be solved in polynomial time.
Cite as

Pascal Schweitzer. Towards an Isomorphism Dichotomy for Hereditary Graph Classes. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 689-702, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schweitzer:LIPIcs.STACS.2015.689,
  author =	{Schweitzer, Pascal},
  title =	{{Towards an Isomorphism Dichotomy for Hereditary Graph Classes}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{689--702},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.689},
  URN =		{urn:nbn:de:0030-drops-49513},
  doi =		{10.4230/LIPIcs.STACS.2015.689},
  annote =	{Keywords: graph isomorphism, modular decomposition, bounded color valence, reductions, forbidden induced subgraphs}
}
Document
DOI: 10.4230/LIPIcs.STACS.2008.1339
On Termination for Faulty Channel Machines

Authors: Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell

Published in: LIPIcs, Volume 1, 25th International Symposium on Theoretical Aspects of Computer Science (2008)

Abstract
A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity.
Cite as

Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, and James Worrell. On Termination for Faulty Channel Machines. In 25th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 1, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.STACS.2008.1339,
  author =	{Bouyer, Patricia and Markey, Nicolas and Ouaknine, Jo\"{e}l and Schnoebelen, Philippe and Worrell, James},
  title =	{{On Termination for Faulty Channel Machines}},
  booktitle =	{25th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{121--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-06-4},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{1},
  editor =	{Albers, Susanne and Weil, Pascal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2008.1339},
  URN =		{urn:nbn:de:0030-drops-13390},
  doi =		{10.4230/LIPIcs.STACS.2008.1339},
  annote =	{Keywords: Automated Verification, Computational Complexity}
}
Document
DOI: 10.4230/DagSemProc.05171.6
Possibilistic Stable Models

Authors: Pascal Nicolas, Laurent Garcia, and Igor Stéphan

Published in: Dagstuhl Seminar Proceedings, Volume 5171, Nonmonotonic Reasoning, Answer Set Programming and Constraints (2005)

Abstract
We present the main lines of a new framework that we have defined in order to improve the knowledge representation power of Answer Set Programming paradigm. Our proposal is to use notions from possibility theory to extend the stable model semantics by taking into account a certainty level, expressed in terms of necessity measure, on each rule of a normal logic program. First of all, we introduce possibilistic definite logic programs and show how to compute the conclusions of such programs both in syntactic and semantic ways. The syntactic handling is done by help of a fix-point operator, the semantic part relies on a possibility distribution on all sets of atoms and the two approaches are shown to be equivalent. In a second part, we define what is a possibilistic stable model for a normal logic program, with default negation. Again, we define a possibility distribution allowing to determine the stable models. We end our presentation by showing how we can use our framework to adressing inconsistency in Answer Set Programming.
Cite as

Pascal Nicolas, Laurent Garcia, and Igor Stéphan. Possibilistic Stable Models. In Nonmonotonic Reasoning, Answer Set Programming and Constraints. Dagstuhl Seminar Proceedings, Volume 5171, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{nicolas_et_al:DagSemProc.05171.6,
  author =	{Nicolas, Pascal and Garcia, Laurent and St\'{e}phan, Igor},
  title =	{{Possibilistic Stable Models}},
  booktitle =	{Nonmonotonic Reasoning, Answer Set Programming and Constraints},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{5171},
  editor =	{Gerhard Brewka and Ilkka Niemel\"{a} and Torsten Schaub and Miroslaw Truszczynski},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05171.6},
  URN =		{urn:nbn:de:0030-drops-2641},
  doi =		{10.4230/DagSemProc.05171.6},
  annote =	{Keywords: Non monotonic reasoning, uncertainty, possibility theory}
}
  • Refine by Author
  • 2 Carrier, Fabienne
  • 2 Halbwachs, Nicolas
  • 2 Jahier, Erwan
  • 2 Maiza, Claire
  • 2 Parent-Vigouroux, Catherine
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Concurrent algorithms
  • 1 Human-centered computing → Asynchronous editors
  • 1 Human-centered computing → Synchronous editors
  • 1 Information systems → Data replication tools
  • 1 Software and its engineering → Real-time systems software
  • Show More...

  • Refine by Keyword
  • 2 graph isomorphism
  • 1 2)
  • 1 Abstract Interpretation
  • 1 Automated Verification
  • 1 Computational Complexity
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 1 2005
  • 1 2008
  • 1 2015
  • 1 2016
  • 1 2017
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact