Re:Software Verification and Analysis Using Z3
by throwawaygh on Saturday January 30, 2021 @08:19PM
(#25974782)
This is called validation, and it's much harder epistemically than verification.
Is it possible to check at runtime that the model is accurate?
Do you have a sensible thing to do if the model isn't accurate (e.g., fallback into "failsafe" mode, let an on-call engineer know that an assumption was violated, etc.)?
Is it possible to check at runtime that the model is accurate?
Do you have a sensible thing to do if the model isn't accurate (e.g., fallback into "failsafe" mode, let an on-call engineer know that an assumption was violated, etc.)?
If yes & yes, well, there's your answer :)