5 ms·

I think the paper provides maybe the best introduction and overview of the approach: http://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf http://www.s3.eurecom.f

I think the paper provides maybe the best introduction and overview of the approach: http://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf http://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf To me, it was also not clear initially why symbolic execution is useful anyway. But this is for testing. The paper introduction explains it. "Symbolic execution was conceived more than 40 years ago to aid in software testing." The goal is to cover all possible execution paths in all possible conditions, which is hard or impossible with traditional testing. The new approach here (SymCC) improves a lot on the runtime of the symbolic execution over previous approaches.

rurban 6y ago
We use cbmc to generate all possible testcases for that. Also with symbolic execution in C, and much better than Klee. http://www.cprover.org/cprover-manual/test-suite/ http://www.cprover.org/cprover-manual/test-suite/
touisteur 6y ago
You can do a lot with Symbolic Execution. Bug-reproduction for example. Say your customer remarks on a weird state if the system. You put a 'stop condition' as 'the system is in the state the customer described' and ask 'how'? You get a list of input & their values. Aaaaah that's how :-). Also if you record/print intermediate values you can use them as complexity reduction for your search. Also, for minimal log/trace placement it's actually fun to use.