2 ms·
Technically 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 int
by lou1306 3y ago
Technically 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