4 ms·
How does symbolic execution w KLEE work to formally verify programs, are there tradeoffs in coverage? For complete coverage you'd have to get it to cover the wh
by zurn 8y ago
How does symbolic execution w KLEE work to formally verify programs, are there tradeoffs in coverage? For complete coverage you'd have to get it to cover the whole possible spaces of states and execution paths of the analyzed system.
- cvwright 8y agoThe 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.