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.
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):
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
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.
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):
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
© 2022 - 2025 — McMap. All rights reserved.
