The way they work around state space explosion is pretty cool. They push all the state off into another module, whose correctness they verify using other metho

The way they work around state space explosion is pretty cool. They push all the state off into another module, whose correctness they verify using other methods. Then they tell the symbolic execution engine that the state-holding module does not misbehave. So it's a hybrid -- use each verification technique where it's strong, to shore up the weaknesses/shortcomings in the other one.