Researcher profile

Clément Aubert

Clément Aubert contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
7topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

7 published item(s)

preprint2022arXiv

A Novel Loop Fission Technique Inspired by Implicit Computational Complexity

This work explores an unexpected application of Implicit Computational Complexity (ICC) to parallelize loops in imperative programs. Thanks to a lightweight dependency analysis, our algorithm allows splitting a loop into multiple loops that can be run in parallel, resulting in gains in terms of execution time similar to state-of-the-art automatic parallelization tools when both are applicable. Our graph-based algorithm is intuitive, language-agnostic, proven correct, and applicable to all types of loops, even if their loop iteration space is unknown statically or at compile time, if they are not in canonical form or if they contain loop-carried dependency. As contributions we deliver the computational technique, proof of its preservation of semantic correctness, and experimental results to quantify the expected performance gains. Our benchmarks also show that the technique could be seamlessly integrated into compiler passes or other automatic parallelization suites. We assert that this original and automatable loop transformation method was discovered thanks to the "orthogonal" approach offered by ICC.

preprint2022arXiv

Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus

This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied $π$-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarity, preserving causality. We point out that corresponding similarity preorders expose clearly distinctions between these semantics. We draw particular attention to the distinguishing power of HP failure similarity, and discuss how it affects the attacker threat model against which we verify security and privacy properties. We also compare existing notions of located bisimilarity to the definitions we introduce.

preprint2022arXiv

mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity

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 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 threefold: 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.

preprint2022arXiv

Proceedings 15th Interaction and Concurrency Experience

This volume contains the proceedings of ICE'22, the 15th Interaction and Concurrency Experience, which was held as an hybrid event in Lucca, Italy, and as a satellite event of DisCoTec'22. The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. The 2022 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Each paper was reviewed by between two and four PC members (with an average of 3.33333333333), and altogether 5 papers were accepted for publication -- plus 3 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Ilaria Castellani and Matthew Parkinson. The abstracts of these talks are included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop.

preprint2022arXiv

Realizing Implicit Computational Complexity

This abstract aims at presenting an ongoing effort to apply a novel typing mechanism stemming from Implicit Computational Complexity (ICC), that tracks dependencies between variables in three different ways, at different stages of maturation.The first and third projects bend the original typing discipline to gain finer-grained view on statements independence, to optimize loops by hoisting invariant and by splitting loops "horizontally" to parallelize them more efficiently.The second project refines and implements the original analysis to obtain a fast, modular static analyzer.All three projects aims at pushing the original type system, inspired from ICC, to its limits, to assess how ICC can in practice leads to original, sometimes orthogonal, approaches.

preprint2020arXiv

How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation

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.

preprint2020arXiv

Structural Equivalences for Reversible Calculi of Communicating Systems (Oral communication)

The formalization of process algebras usually starts with a minimal core of operators and rules for its transition system, and then relax the system to improve its usability and ease the proofs. In the calculus of communicating systems (CCS), the structural congruence plays this role by making e.g. parallel composition commutative and associative: without it, the system would be cumbersome to use and reason about, and it can be proven that this change is innocuous in a precise technical sense. For the two reversible calculi extending CCS, the situation is less clear: CCS with Communication Keys (CCSK) was first defined without any structural congruence, and then was endowed with a fragment of CCS's congruence. Reversible CCS (RCCS) made the choice of "backing in" the structural equivalence, that became part of the "minimal core" of the system. In this short oral communication, we would like to re-consider the status and role of the structural congruence in general, to question its role in RCCS in particular, and to ask the more general question of the structural equivalences legitimacy.