Wendelin Serwe
A grouping.
Wendelin Serwe -- Inria Grenoble, with the CADP group. Three records, none of them first-authored by him, spanning eleven years, and read in order they are a single sustained attempt to make an industrial-strength process-algebra toolbox reach asynchronous circuits as designers actually write them.
2009 garavel2009semantics CHP given a structural operational semantics, then translated into LOTOS for CADP 2018 bouzafour2018modelchecking a synthesisable SystemVerilog subset mapped into LNT for CADP 2020 mateescu2020modeling a patented industrial shield circuit modelled in LNT and EXP, at two levels
**What the line is actually about.** Not a verification technique -- CADP already existed -- but the distance between it and a circuit. Every one of these records rests on a translation. Two of them -- garavel2009semantics and bouzafour2018modelchecking -- sit in the-cost-is-in-the-translation because there the translation *is* the contribution. mateescu2020modeling was considered for that set and left out: its hand modelling in LNT is a prerequisite rather than the result, and on that reading almost any model-checking paper would qualify, which would empty the rule of content. The target language moves (LOTOS, then LNT) and the source language moves (CHP, then SystemVerilog, then a netlist modelled by hand), but the work is always the same work: restating hardware in a language a process-algebra checker can hold.
**The eleven years are the argument.** If translation were a solved step it would not be the headline contribution of a journal paper in 2009 and again of a conference paper in 2018. And the two do not simply repeat: garavel2009semantics reports an implemented translator, while bouzafour2018modelchecking applied its SystemVerilog-to-LNT mapping **by hand** to a 4000-line industrial memory protection unit, listing automation as future work "while eliminating the potential errors that may arise from manual translation". So what the later model checker proved holds of a model a person wrote from the design, not of the design. That pair is the clearest evidence in this corpus that the step is neither trivial nor reliably automated even by the people who have done it before.
**Where the line arrives.** mateescu2020modeling is the payoff and the most interesting of the three, because it reports what each abstraction level could and could not do. The circuit is a shield patented by Tiempo Secure, laid over another asynchronous circuit to protect it against physical attack -- cutting a wire, forcing a wire to a constant voltage, shorting two wires together. Modelled at circuit level, an induction proof extends the attack analysis to a shield of **arbitrary size**; modelled at gate level, no comparable result, "due to the necessity of stubs". Refine the model and the general theorem is lost. And the analysis *discovered* the isochronic fork assumption rather than assuming it -- CADP reported that without isochrony of forks the shield does not behave as intended, which is the same irreducible concession quasi-delay-insensitive design makes by classification, arrived at here by state-space exploration.
**Why a person set for a third author is worth having.** Serwe is never the first name and the corpus would not surface him by any ordinary search, yet he is the continuity: Garavel appears on the first two, Mateescu on the last two, Renaudin and Bouzafour on the last two, and only Serwe is on all three. The line's persistence is visible through him and not through any of the others.
Overlaps the-cost-is-in-the-translation, which holds the first two for the translation itself, and hardware-security, where the 2020 shield sits. The nearest neighbour outside CADP is bouzafour2018modelchecking's own subject matter -- asynchronous and quasi-delay-insensitive design -- where this corpus holds the classification results these papers verify against.