Stainless PipelineUserFrontendCompilerCallBackRegistryComponentUse ICG: Incremental Computational GraphVerification and/orTermination;Run in threadsVerification and/orTerminationdotc, scalac, ...Update Code;Run FrontendRun CompilerTypecheckCompilation Unit(xlang.Trees)Register newFunDef & ClassDefUse ICG to identifywhat is ready orneed to be recomputed.Option[self-containedprogram]transform trees, generate VCs, send to the solvers, ...The "loop" is executed once more to trigger the verification ofnon-sealed classes now that all the overridden functions are known.wait for Component's ReportsReports...Reports...Reports...All ReportsDisplay reportsunder --watch modethe process restart.The Registry's ICG is the center piece thatenables stainless to verify modified functionswhen the code is updated.loop[for each compilation unit]opt[solve]