In formal verification, case splitting consists of separately considering different cases.
In symbolic evaluation, case splitting introduces multiple paths where some variable has a different concrete value on each path. This allows more efficient reasoning about concrete values and can work past issues that would be hard for a solver to handle such as non-linearity, etc.
Notes related to Case splitting
State merging, Swarm verification, Verification performance of code, Verification profiling of code, Verifier performance
Papers related to Case splitting
- Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
- Evaluating manual intervention to address the challenges of bug finding with KLEE [galea:arxiv:2018]
- A synergistic approach for distributed symbolic execution using test ranges [qiu:icse:2017]
- Using test ranges to improve symbolic execution [qiu:nfm:2018]
- Scaling symbolic execution using ranged analysis [siddiqui:oopsla:2012]
- A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]
- Chopped symbolic execution [trabish:icse:2018]