Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs).
The question is what do they do and how do they work.
You first have your source code for some application. You then transform your source code into some state-transition graph like a Kripke Structure. The states are filled with atomic propositions which describe what is true in that particular state. In Symbolic Model Checking the atomic propositions are encoded as OBDDs to save on space and improve performance.
The Model Checker then starts at some initial state, and explores the states, looking for errors in the state-transition graph. If it finds an error it will often generate a test case demonstrating the error. It uses the symbolic OBDDs to somewhat optimally navigate the state space. Wish I could explain more there but still learning.
But that's basically it. You have a program converted into a formal model (state-transition graph), and then you use symbolic optimizations to navigate the state space to look for errors (by comparing it against an LTL/CTL specification). And if an error is found, the Model Checker gives you some stuff to help document and solve it.