18 Search Results for "Merz, Stephan"


Volume

OASIcs, Volume 3

Workshop on Trustworthy Software

TrustworthySW 2006, May 18-19, 2006, Saarbruecken, Germany

Editors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper

Document
Self-Stabilizing Clock Synchronization in Probabilistic Networks

Authors: Bernadette Charron-Bost and Louis Penet de Monterno

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)


Abstract
We consider the fundamental problem of clock synchronization in a synchronous multi-agent system. Each agent holds a clock with an arbitrary initial value, and clocks must eventually indicate the same value, modulo some integer P. A known solution for this problem in dynamic networks is the self-stabilization SAP (for self-adaptive period) algorithm, which uses finite memory and relies solely on the assumption of a finite dynamic diameter in the communication network. This paper extends the results on this algorithm to probabilistic communication networks: We introduce the concept of strong connectivity with high probability and we demonstrate that in any probabilistic communication network satisfying this hypothesis, the SAP algorithm synchronizes clocks with high probability. The proof of such a probabilistic hyperproperty is based on novel tools and relies on weak assumptions about the probabilistic communication network, making it applicable to a wide range of networks, including the classical push model. We provide an upper bound on time and space complexity. Building upon previous works by Feige et al. and Pittel, the paper provides solvability results and evaluates the stabilization time and space complexity of SAP in two specific cases of communication topologies.

Cite as

Bernadette Charron-Bost and Louis Penet de Monterno. Self-Stabilizing Clock Synchronization in Probabilistic Networks. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{charronbost_et_al:LIPIcs.DISC.2023.12,
  author =	{Charron-Bost, Bernadette and Penet de Monterno, Louis},
  title =	{{Self-Stabilizing Clock Synchronization in Probabilistic Networks}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.12},
  URN =		{urn:nbn:de:0030-drops-191389},
  doi =		{10.4230/LIPIcs.DISC.2023.12},
  annote =	{Keywords: Self-stabilization, Clock synchronization, Probabilistic networks}
}
Document
Self-Stabilizing Clock Synchronization in Dynamic Networks

Authors: Bernadette Charron-Bost and Louis Penet de Monterno

Published in: LIPIcs, Volume 253, 26th International Conference on Principles of Distributed Systems (OPODIS 2022)


Abstract
We consider the fundamental problem of periodic clock synchronization in a synchronous multi-agent system. Each agent holds a clock with an arbitrary initial value, and clocks must eventually be congruent, modulo some positive integer P. Previous algorithms worked in static networks with drastic connectivity properties and assumed that global informations are available at each node. In this paper, we propose a finite-state algorithm for time-varying topologies that does not require any global knowledge on the network. The only assumption is the existence of some integer D such that any two nodes can communicate in each sequence of D consecutive rounds, which extends the notion of strong connectivity in static network to dynamic communication patterns. The smallest such D is called the dynamic diameter of the network. If an upper bound on the diameter is provided, then our algorithm achieves synchronization within 3D rounds, whatever the value of the upper bound. Otherwise, using an adaptive mechanism, synchronization is achieved with little performance overhead. Our algorithm is parameterized by a function g, which can be tuned to favor either time or space complexity. Then, we explore a further relaxation of the connectivity requirement: our algorithm still works if there exists a positive integer R such that the network is rooted over each sequence of R consecutive rounds, and if eventually the set of roots is stable. In particular, it works in any rooted static network.

Cite as

Bernadette Charron-Bost and Louis Penet de Monterno. Self-Stabilizing Clock Synchronization in Dynamic Networks. In 26th International Conference on Principles of Distributed Systems (OPODIS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 253, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{charronbost_et_al:LIPIcs.OPODIS.2022.28,
  author =	{Charron-Bost, Bernadette and Penet de Monterno, Louis},
  title =	{{Self-Stabilizing Clock Synchronization in Dynamic Networks}},
  booktitle =	{26th International Conference on Principles of Distributed Systems (OPODIS 2022)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-265-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{253},
  editor =	{Hillel, Eshcar and Palmieri, Roberto and Rivi\`{e}re, Etienne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2022.28},
  URN =		{urn:nbn:de:0030-drops-176480},
  doi =		{10.4230/LIPIcs.OPODIS.2022.28},
  annote =	{Keywords: Self-stabilization, Clock synchronization, Dynamic networks}
}
Document
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle

Authors: Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry

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


Abstract
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.

Cite as

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2019.13,
  author =	{Chen, Ran and Cohen, Cyril and L\'{e}vy, Jean-Jacques and Merz, Stephan and Th\'{e}ry, Laurent},
  title =	{{Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{13:1--13: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.13},
  URN =		{urn:nbn:de:0030-drops-110683},
  doi =		{10.4230/LIPIcs.ITP.2019.13},
  annote =	{Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification}
}
Document
Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141)

Authors: Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, and Josef Widder

Published in: Dagstuhl Reports, Volume 3, Issue 4 (2013)


Abstract
The Dagstuhl Seminar 13141 "Formal Verification of Distributed Algorithms" brought together researchers from the areas of distributed algorithms, model checking, and semi-automated proofs with the goal to establish a common base for approaching the many open problems in verification of distributed algorithms. In order to tighten the gap between the involved communities, who have been quite separated in the past, the program contained tutorials on the basics of the concerned fields. In addition to technical talks, we also had several discussion sessions, whose goal was to identify the most pressing research challenges. This report describes the program and the outcomes of the seminar.

Cite as

Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, and Josef Widder. Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). In Dagstuhl Reports, Volume 3, Issue 4, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@Article{charronbost_et_al:DagRep.3.4.1,
  author =	{Charron-Bost, Bernadette and Merz, Stephan and Rybalchenko, Andrey and Widder, Josef},
  title =	{{Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141)}},
  pages =	{1--16},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{4},
  editor =	{Charron-Bost, Bernadette and Merz, Stephan and Rybalchenko, Andrey and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.4.1},
  URN =		{urn:nbn:de:0030-drops-40747},
  doi =		{10.4230/DagRep.3.4.1},
  annote =	{Keywords: Distributed algorithms; semi-automated proofs; model checking}
}
Document
Complete Volume
OASIcs, Volume 3, Trustworthy SW'06, Complete Volume

Authors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
OASIcs, Volume 3, Trustworthy SW'06, Complete Volume

Cite as

Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@Proceedings{autexier_et_al:OASIcs.TrustworthySW.2006,
  title =	{{OASIcs, Volume 3, Trustworthy SW'06, Complete Volume}},
  booktitle =	{Workshop on Trustworthy Software},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006},
  URN =		{urn:nbn:de:0030-drops-35659},
  doi =		{10.4230/OASIcs.TrustworthySW.2006},
  annote =	{Keywords: Software/Program Verification}
}
Document
An Introduction to the Tool Ticc

Authors: Axel Legay, Luca de Alfaro, and Marco Faella

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
This paper is a tutorial introduction to the sociable interface model of [12] and its underlying tool \textsc{Tcc}. The paper starts with a survey of the theory of interfaces and then introduces the sociable interface model that is a game-based model with rich communication primitives to facilitate the modeling of software and distributed systems. The model and its main features are then intensivelly discussed and illustrated using the tool \textsc{Tcc}.

Cite as

Axel Legay, Luca de Alfaro, and Marco Faella. An Introduction to the Tool Ticc. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{legay_et_al:OASIcs.TrustworthySW.2006.766,
  author =	{Legay, Axel and de Alfaro, Luca and Faella, Marco},
  title =	{{An Introduction to the Tool Ticc}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--32},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.766},
  URN =		{urn:nbn:de:0030-drops-7667},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.766},
  annote =	{Keywords: Open system, game, interface automata}
}
Document
Abstracts Collection -- Workshop Trustworthy Software 2006

Authors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
On 18-19 May 2006, the Saarland University organized a two-day workshop about "Trustworthy Software" in order to present and foster the research competence in the SaarLorLuxWallonie region in the area of developing safe, secure and reliable software, computers and networks. As part of the Interreg III C E-Bird project "Recherches sans fronti\`eres/Forschen ohne Grenzen" it provided an excellent forum especially for young scientists to present and discuss recent results, new ideas and future research directions to a transnational audience from the SaarLorLuxWallonie region. The workshop consisted of 21 regular presentations and one invited talk. Abstracts of all presentations are collected in this paper, including links to extended abstracts or full papers. The first section directs to the preface of the proceedings.

Cite as

Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper. Abstracts Collection -- Workshop Trustworthy Software 2006. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{autexier_et_al:OASIcs.TrustworthySW.2006.758,
  author =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  title =	{{Abstracts Collection -- Workshop Trustworthy Software 2006}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--7},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.758},
  URN =		{urn:nbn:de:0030-drops-7588},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.758},
  annote =	{Keywords: Software evolution, Modularity, Automated debugging, Dependability assurance, Failure analysis, Static program analysis, Infinite and Finite-state verification, Runtime verification, Theorem proving, Access control, Security analysis, Security protocols, E-Voting}
}
Document
Front Matter
Preface -- Workshop Trustworthy Software 2006

Authors: Serge Autexier, Stephan Merz, Leon van der Torre, Reinhard Wilhelm, and Pierre Wolper

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
As part of the Interreg III C/E-Bird project "Recherches sans fronti\`eres/Forschen ohne Grenzen" the Saarland University organized a two-day workshop about "Trustworthy Software" in order to present and foster the research competence in the SaarLorLuxWallonie region in the area of developing safe, secure and reliable software, computers and networks. The workshop especially provided a forum for young scientists to present their research to a transnational audience from the SaarLorLuxWallonie region and consisted of 21 regular presentations and one invited presentation.

Cite as

Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. i-vi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{autexier_et_al:OASIcs.TrustworthySW.2006.693,
  author =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  title =	{{Preface -- Workshop Trustworthy Software 2006}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{i--vi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.693},
  URN =		{urn:nbn:de:0030-drops-6932},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.693},
  annote =	{Keywords: Trustworthy software, preface}
}
Document
An Operator-based Approach to Incremental Development of Conform Protocol State Machines

Authors: Arnaud Lanoix, Dieu-Donné Okalas Ossami, and Jeanine Souquières

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
An incremental development framework which supports a conform construction of Protocol State Machines (PSMs) is presented. We capture design concepts and strategies of PSM construction by sequentially applying some development operators: each operator makes evolve the current PSM to another one. To ensure a conform construction, we introduce three conformance relations, inspired by the specification refinement and specification matchings supported by formal methods. Conformance relations preserve some global behavioral properties. Our purpose is illustrated by some development steps of the card service interface of an electronic purse: for each step, we introduce the idea of the development, we propose an operator and we give the new specification state obtained by the application of this operator and the property of this state relatively to the previous one in terms of conformance relation.

Cite as

Arnaud Lanoix, Dieu-Donné Okalas Ossami, and Jeanine Souquières. An Operator-based Approach to Incremental Development of Conform Protocol State Machines. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{lanoix_et_al:OASIcs.TrustworthySW.2006.695,
  author =	{Lanoix, Arnaud and Okalas Ossami, Dieu-Donn\'{e} and Souqui\`{e}res, Jeanine},
  title =	{{An Operator-based Approach to Incremental Development of Conform Protocol State Machines}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.695},
  URN =		{urn:nbn:de:0030-drops-6953},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.695},
  annote =	{Keywords: Protocol state machine, incremental development, development operator, exact conformance, plugin conformance, partial conformance}
}
Document
Explaining Data Type Reduction in the Shape Analysis Framework

Authors: Björn Wachter

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
Automatic formal verification of systems composed of a large or even unbounded number of components is difficult as the state space of these systems is prohibitively large. Abstraction techniques automatically construct finite approximations of infinite-state systems from which safe information about the original system can be inferred. We study two abstraction techniques shape analysis, a technique from program analysis, and data type reduction, originating from model checking. Until recently we did not properly understand how shape analysis and data type reduction relate. In this talk, we shed light on this relation in a comprehensive way. This is a step towards a more unified view of abstraction employed in the static analysis and model checking community.

Cite as

Björn Wachter. Explaining Data Type Reduction in the Shape Analysis Framework. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{wachter:OASIcs.TrustworthySW.2006.701,
  author =	{Wachter, Bj\"{o}rn},
  title =	{{Explaining Data Type Reduction in the Shape Analysis Framework}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.701},
  URN =		{urn:nbn:de:0030-drops-7016},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.701},
  annote =	{Keywords: Canonical abstraction, data type reduction, model checking, parameterized system, infinite-state}
}
Document
Formal Validation of Pattern Matching code

Authors: Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
When addressing the formal validation of generated software, two main alternatives consist either to prove the correctness of compilers or to directly validate the generated code. Here, we focus on directly proving the correctness of compiled code issued from powerful pattern matching constructions typical of ML like languages or rewrite based languages such as ELAN, MAUDE or Tom. In this context, our first contribution is to define a general framework for anchoring algebraic pattern-matching capabilities in existing languages like C, Java or ML. Then, using a just enough powerful intermediate language, we formalize the behavior of compiled code and define the correctness of compiled code with respect to pattern-matching behavior. This allows us to prove the equivalence of compiled code correctness with a generic first-order proposition whose proof could be achieved via a proof assistant or an automated theorem prover. We then extend these results to the multi-match situation characteristic of the ML like languages. The whole approach has been implemented on top of the Tom compiler and used to validate the syntactic matching code of the Tom compiler itself.

Cite as

Claude Kirchner, Pierre-Etienne Moreau, and Antoine Reilles. Formal Validation of Pattern Matching code. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{kirchner_et_al:OASIcs.TrustworthySW.2006.697,
  author =	{Kirchner, Claude and Moreau, Pierre-Etienne and Reilles, Antoine},
  title =	{{Formal Validation of Pattern Matching code}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.697},
  URN =		{urn:nbn:de:0030-drops-6978},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.697},
  annote =	{Keywords: Correctness proofs, compilers, pattern matching, validation}
}
Document
Formalizing On Chip Communications in a Functional Style

Authors: Julien Schmaltz and Dominique Borrione

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
This paper presents a formal model for representing {it any} on-chip communication architecture. This model is described mathematically by a function, named $mathit{GeNoC}$. The correctness of $mathit{GeNoC}$ is expressed as a theorem, which states that messages emitted on the architecture reach their expected destination without modification of their content. The model identifies the key constituents common to {it all} communication architectures and their essential properties, from which the proof of the $GeNoC$ theorem is deduced. Each constituent is represented by a function which has no {it explicit} definition but is constrained to satisfy the essential properties. Thus, the validation of a {it particular} architecture is reduced to the proof that its concrete definition satisfies the essential properties. In practice, the model has been defined in the logic of the ACL2 theorem proving system. We define a methodology that yields a systematic approach to the validation of communication architectures at a high level of abstraction. To validate our approach, we exhibit several architectures that constitute concrete instances of the generic model $GeNoC$. Some of these applications come from industrial designs, such as the AMBA AHB bus or the Octagon network from ST Microelectronics.

Cite as

Julien Schmaltz and Dominique Borrione. Formalizing On Chip Communications in a Functional Style. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{schmaltz_et_al:OASIcs.TrustworthySW.2006.700,
  author =	{Schmaltz, Julien and Borrione, Dominique},
  title =	{{Formalizing On Chip Communications in a Functional Style}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--25},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.700},
  URN =		{urn:nbn:de:0030-drops-7000},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.700},
  annote =	{Keywords: SoC's, communication architectures, formal methods, automated theorem proving}
}
Document
Isolating Intrusions by Automatic Experiments

Authors: Stephan Neuhaus

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
When dealing with malware infections, one of the first tasks is to find the processes that were involved in the attack. We introduce Malfor, a system that isolates those processes automatically. In contrast to other methods that help analyze attacks, Malfor works by experiments: first, we record the interaction of the system under attack; after the intrusion has been detected, we replay the recorded events in slightly different configurations to see which processes were relevant for the intrusion. This approach has three advantages over deductive approaches: first, the processes that are thus found have been experimentally shown to be relevant for the attack; second, the amount of evidence that must then be analyzed to find the attack vector is greatly reduced; and third, Malfor itself cannot make wrong deductions. In a first experiment, Malfor was able to extract the three processes responsible for an attack from 32 candidates in about six minutes.

Cite as

Stephan Neuhaus. Isolating Intrusions by Automatic Experiments. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{neuhaus:OASIcs.TrustworthySW.2006.696,
  author =	{Neuhaus, Stephan},
  title =	{{Isolating Intrusions by Automatic Experiments}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--3},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.696},
  URN =		{urn:nbn:de:0030-drops-6960},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.696},
  annote =	{Keywords: Intrusion Analysis, Malware, Experimentation}
}
Document
Relating two standard notions of secrecy

Authors: Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)


Abstract
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data { t s}. Reach-ability-based secrecy means that { t s} should never be disclosed while equi-valence-based secrecy states that two executions of a protocol with distinct instances for { t s} should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far. This paper initiates a systematic investigation of situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries in the case of symmetric encryption, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.

Cite as

Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch. Relating two standard notions of secrecy. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


Copy BibTex To Clipboard

@InProceedings{zalinescu_et_al:OASIcs.TrustworthySW.2006.691,
  author =	{Zalinescu, Eugen and Cortier, V\'{e}ronique and Rusinowitch, Micha\"{e}l},
  title =	{{Relating two standard notions of secrecy}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.691},
  URN =		{urn:nbn:de:0030-drops-6911},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.691},
  annote =	{Keywords: Verification, security protocols, secrecy, applied-pi calculus}
}
  • Refine by Author
  • 5 Merz, Stephan
  • 3 Autexier, Serge
  • 3 Charron-Bost, Bernadette
  • 3 Wilhelm, Reinhard
  • 3 Wolper, Pierre
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Distributed algorithms
  • 2 Theory of computation → Dynamic graph algorithms
  • 1 Software and its engineering → Formal software verification

  • Refine by Keyword
  • 2 Clock synchronization
  • 2 Self-stabilization
  • 1 Abstraction
  • 1 Access control
  • 1 Artificial Cell Communication
  • Show More...

  • Refine by Type
  • 17 document
  • 1 volume

  • Refine by Publication Year
  • 13 2006
  • 2 2023
  • 1 2012
  • 1 2013
  • 1 2019

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