Menu
Recently, I started to study formal verification techniques. In literature, model checker and solver are used somehow interchangeably. But, how model checker and solver are connected with each other?
p.s. I would appreciate if some papers or links are suggested.
566
Boolean Satisfiability (SAT) solvers determine the 'satisfiability' of boolean set of equations for a set of inputs. An SMT solver Satisfiability Modulo a Theory) applies SMT to bit-vectors, strings, arrays, and more. Together, we can reduce a program and prove it is satisfiable, or provide a concrete counter-example.
At a high level, an SMT solver takes as input a first-order logical formula and then tries to decide if the formula is satisfiable. In the process, solvers employ various heuristics that first transform the input formula into a suitable representation and then use search procedures to check for satisfiability.
Bounded model-checking algorithms unroll the FSM for a fixed number of steps, , and check whether a property violation can occur in or fewer steps. This typically involves encoding the restricted model as an instance of SAT.
In model checking, you have a model and a specification (or property), and you check if the model meets the specification.
In SAT solving, you have a formula and you try to find a satisfying assignment to it.
Now, in model checking, you can conjunct the model and the negation of the property to give you one formula. Use a solver to solve for this formula. If it gives you a solution, it would mean the property is sometimes violated (since you conjuncted the negated property). Getting unsat would mean your model satisfies the property/specification.
123
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
