Hubert Garavel

A grouping.

Hubert Garavel, INRIA Grenoble, the long-running lead of the **CADP** toolbox. Four records, and they divide unusually cleanly into two activities that most researchers do not combine: building verification technology for concurrency, and asking the field to account for itself.

**The tool line, applied to hardware.** garavel2009semantics gives value-passing CHP -- the calculus martin1986compiling compiles into delay-insensitive circuits -- a structural operational semantics that admits channels open to the environment and is independent of the handshake protocol, then translates it into LOTOS so CADP can verify it; an implemented translator was used for compositional verification of an asynchronous DES and a network-on-chip interconnect. bouzafour2018modelchecking does the same job nine years later for a synthesisable SystemVerilog subset into LNT, on an industrial memory protection unit, with the mapping applied by hand. Alongside them, though not his own, mateescu2020modeling applies the same toolbox to an asynchronous circuit for fault protection. Together they are this corpus's clearest evidence that a concurrency-theory toolbox can be pointed at real asynchronous hardware -- and, in the 2018 paper's own future work, of what is still missing between the design and the model.

**The survey line, which is rarer and is why this set is worth having.** garavel2020expert is an expert survey on the state of formal methods, and beek2024formal is on formal methods in industry. Most people who build a verification tool publish results obtained with it; comparatively few go and ask a field what it actually believes and uses. Set those beside toma2006verification's figures on verification cost and bouzafour2018modelchecking's complaint that formal verification "is not widespread enough, as many hardware designers are not familiar with it", and the corpus has both the anecdote and the survey.

The pairing matters for a bibliography about hardware verification specifically: it is easy to assemble a corpus of successful verifications and conclude the problem is solved. Records that measure adoption are the correction, and this author supplies both halves.