+++
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