Stijn de Gouw
14 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.
Stijn de Gouw
Deductive verification of production Java with KeY, and the claim behind it: that proof finds defects in code already shipped and widely trusted, not only in code written to be verified. The result the work is built around is the demonstration that OpenJDK's sorting routine could not meet its specification, held here with the proof that preceded it and the completed verification that followed; the LinkedList and abstract-data-type verifications apply the same method again. Two records step outside to footprint and dynamic separation logic, approaching the same programs through what a component may touch. dblp: https://dblp.org/pid/34/11095