Search Results

Documents authored by Aubert, Clément

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.30
Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus

Authors: Clément Aubert, Ross Horne, and Christian Johansen

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We introduce a non-interleaving structural operational semantics for the applied π-calculus and prove that it satisfies the properties expected of a labelled asynchronous transition system (LATS). LATS have well-studied relations with other standard non-interleaving models, such as Mazurkiewicz traces or event structures, and are a natural extension of labelled transition systems where the independence of transitions is made explicit. We build on a considerable body of literature on located semantics for process algebras and adopt a static view on locations to identify the parallel processes that perform a transition. By lifting, in this way, work on CCS and π-calculus to the applied π-calculus, we lay down a principled foundation for reusing verification techniques such as partial-order reduction and non-interleaving equivalences in the field of security. The key technical device we develop is the notion of located aliases to refer unambiguously to a specific output originating from a specific process. This light mechanism ensures stability, avoiding disjunctive causality problems that parallel extrusion incurs in similar non-interleaving semantics for the π-calculus.
Cite as

Clément Aubert, Ross Horne, and Christian Johansen. Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aubert_et_al:LIPIcs.CONCUR.2022.30,
  author =	{Aubert, Cl\'{e}ment and Horne, Ross and Johansen, Christian},
  title =	{{Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{30:1--30:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.30},
  URN =		{urn:nbn:de:0030-drops-170930},
  doi =		{10.4230/LIPIcs.CONCUR.2022.30},
  annote =	{Keywords: Security, Processes, Structural operational semantics, Asynchronous transition systems, Applied pi-calculus}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.26
mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity

Authors: Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Implicit Computational Complexity (ICC) drives better understanding of complexity classes, but it also guides the development of resources-aware languages and static source code analyzers. Among the methods developed, the mwp-flow analysis [Jones and Lars Kristiansen, 2009] certifies polynomial bounds on the size of the values manipulated by an imperative program. This result is obtained by bounding the transitions between states instead of focusing on states in isolation, as most static analyzers do, and is not concerned with termination or tight bounds on values. Those differences, along with its built-in compositionality, make the mwp-flow analysis a good target for determining how ICC-inspired techniques diverge compared with more traditional static analysis methods. This paper’s contributions are three-fold: we fine-tune the internal machinery of the original analysis to make it tractable in practice; we extend the analysis to function calls and leverage its machinery to compute the result of the analysis efficiently; and we implement the resulting analysis as a lightweight tool to automatically perform data-size analysis of C programs. This documented effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that furthermore decorrelates the problem of deciding if a bound exist with the problem of computing it.
Cite as

Clément Aubert, Thomas Rubiano, Neea Rusch, and Thomas Seiller. mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 26:1-26:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{aubert_et_al:LIPIcs.FSCD.2022.26,
  author =	{Aubert, Cl\'{e}ment and Rubiano, Thomas and Rusch, Neea and Seiller, Thomas},
  title =	{{mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{26:1--26:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.26},
  URN =		{urn:nbn:de:0030-drops-163071},
  doi =		{10.4230/LIPIcs.FSCD.2022.26},
  annote =	{Keywords: Static Program Analysis, Implicit Computational Complexity, Automatic Complexity Analysis, Program Verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.7
How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation

Authors: Clément Aubert and Ioana Cristescu

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Reversible computation opens up the possibility of overcoming some of the hardware’s current physical limitations. It also offers theoretical insights, as it enriches multiple paradigms and models of computation, and sometimes retrospectively enlightens them. Concurrent reversible computation, for instance, offered interesting extensions to the Calculus of Communicating Systems, but was still lacking a natural and pertinent bisimulation to study processes equivalences. Our paper formulates an equivalence exploiting the two aspects of reversibility: backward moves and memory mechanisms. This bisimulation captures classical equivalences relations for denotational models of concurrency (history- and hereditary history-preserving bisimulation, (H)HPB), that were up to now only partially characterized by process algebras. This result gives an insight on the expressiveness of reversibility, as both backward moves and a memory mechanism - providing "backward determinism" - are needed to capture HHPB.
Cite as

Clément Aubert and Ioana Cristescu. How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aubert_et_al:LIPIcs.CONCUR.2020.7,
  author =	{Aubert, Cl\'{e}ment and Cristescu, Ioana},
  title =	{{How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.7},
  URN =		{urn:nbn:de:0030-drops-128196},
  doi =		{10.4230/LIPIcs.CONCUR.2020.7},
  annote =	{Keywords: Formal semantics, Process algebras and calculi, Distributed and reversible computation, Configuration structures, Reversible CCS, Bisimulation}
}
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 About DROPS Imprint Privacy Contact