CODEWITHSUNDEEP
solversmtmodel-checkingsat
shahb0z
shahb0z

Reputation: 73

SMT/SAT Solver vs Model Checker

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.

Upvotes: 6

Views: 2180

Answers (2)

Sukanya B
Sukanya B

Reputation: 506

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.

Upvotes: 6

goofy
goofy

Reputation: 559

To perform model checking a reachability analysis is needed and to do this the program transitions are often executed symbolically. The solution to the resulting satisfaction problem is created by a solver. A very basic and very good introduction is found in this free text book (Part III: Analysis and Verification):

http://leeseshia.org

Edward A. Lee and Sanjit A. Seshia, Introduction to Embedded Systems, A Cyber-Physical Systems Approach, Second Edition, MIT Press, ISBN 978-0-262-53381-2, 2017

Upvotes: 3

Related Questions