3 ms·
> however runs all possible executions, No, it does not. It probably does constraint based verification or looks for "proofs" of possible error conditions or a
by jvanderbot 3y ago
> however runs all possible executions,
No, it does not. It probably does constraint based verification or looks for "proofs" of possible error conditions or asserts. In the case shown, an uninitialized variable is trivial to prove that it could equal the asseted value.
- philzook 3y agoYes, correct. It does not and could not _actually_ run all possible executions unless the program state space is quite small. But from a user's perspective, it is similar. I have tried this pedagogical approach to describing verifiers like these as "infinite" unit tests before (to mixed results). It feels to me that what symbolic or constraint based reasoning (algebraic identities, programs, integrals, what have you) in general is doing is finding a way to finitely reason about a very large or actually infinite number of concretized cases.
- lou1306 3y agoTechnically speaking it a) unrolls all loop up to their length (if it can be statically determined) or to a given verification bound; b) transforms the code into SSA; c) transforms the SSA into a SAT formula. If the SAT formula is satisfiable, its certificate is a counterexample to the property under verifecation. Of course the toy example is a toy, and of course it does not "run" anything, but this is a sound technique: if there is an execution that violates a property, it will be found. I highly suggest reading the paper that introduced it [1], it is remarkably clear! [1] Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS), 2004, Barcelona, Spain. Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15 https://doi.org/10.1007/978-3-540-24730-2_15