diff options
Diffstat (limited to 'content/zettel/3a8g5g.md')
| -rw-r--r-- | content/zettel/3a8g5g.md | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/content/zettel/3a8g5g.md b/content/zettel/3a8g5g.md new file mode 100644 index 0000000..e258e49 --- /dev/null +++ b/content/zettel/3a8g5g.md @@ -0,0 +1,19 @@ ++++ +title = "Using a SAT solver to prove correctness of predicates" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3g6a", "3a8g5f", "3a8g5e2"] +forwardlinks = ["3a8g5e", "3a8g5h", "3a8g5g1"] +zettelid = "3a8g5g" ++++ + +As mentioned in the proof of validation ([\#3a8g5e]) A SAT solver can be +used to prove the predicate property for all of the program points. +However, the main problem is that the predicates can sometimes be large +and the checking, especially with a naïve SAT solver that is proven +correct. However, it should be possible to use a SAT solver like Z3 to +simplify the predicate when it is constructed, so that the checking time +is minimised. + + [\#3a8g5e]: /zettel/3a8g5e |