Oussama Oulkaid

A grouping.

Oussama Oulkaid, whose CIFRE industrial doctorate ran between Lyon LIP, Grenoble VERIMAG and the electrical-verification vendor Aniah. Five records, and they are the corpus's only sustained treatment of formal verification applied **below the logic level** -- at the transistor, against electrical rules, rather than against functional specifications.

2023 ferres2023electrical electrical rule checking by satisfiability 2024 oulkaid2024transistor a relational transistor-level semantics, discharged with Z3 2025 oulkaid2025modeles the thesis: three semantics defined and measured against each other 2025 ferres2025survey the survey of transistor-level electrical rule checking 2026 oulkaid2026modeling the journal paper: electrical overstress, and a correction to the thesis

**Why this line matters to the rest of the corpus.** Nearly everything else held here verifies a circuit against what it should *compute*. These records verify it against what it may electrically *do* -- missing level-shifters, electrical overstress, the failures that a functionally correct netlist can still commit. the-switch-or-the-curve asks how much of the device a correctness argument admits; this work is the case where the argument admits the I-V characteristic itself and then has to decide how to approximate it.

**The thesis's most-quoted result is the one most often quoted wrongly, and the corpus has the correction.** oulkaid2025modeles defines three semantics and reports that the one tracking SPICE most closely is **unsound**, because its linear approximations are not conservative. Cited bare, that reads as a verdict on modelling electrical behaviour at all. oulkaid2026modeling traces it to the *shape* of the approximation -- quarter-planes -- and proposes a conservative envelope of the I-V curve, a union of polyhedra, as the repair. That repair is stated as future work and **is not done**. Anyone citing the unsoundness finding should cite the journal paper beside it; the two records are linked on the corpus so the pairing is unavoidable.

**What the thesis does that its papers do not.** oulkaid2024transistor states the switch-based relational semantics compactly and demonstrates it on missing level-shifters in large industrial circuits; the thesis defines two further semantics alongside it and measures all three on **time, memory and soundness** across three error classes. Method papers rarely publish the losing configurations, and the comparison is why the thesis is worth reading even where the papers exist.

Bruno Ferres is the co-author across the group's other two records, including the survey, which is where a reader new to electrical rule checking should start. The industrial partner is not incidental: the circuits are large, real, and the error classes are the ones a vendor is paid to find.