Following the terminology in section 3.1 of bornholt:oopsla:2018, “symbolic evaluation” is a generalization of bounded model checking consisting of exploring some paths through a program collecting symbolic path constraints from conditional branches.
In symbolic execution, a single path is followed at a time which has the advantage that states do not need to be merged at join points and so many calculations involve concrete values and so can be evaluated directly and efficiently.
In bounded model checking, all paths are followed at a time so states have to be merged at join points resulting in many symbolic values but, with the advantage that it avoids the path explosion problem seen in symbolic execution.
Notes related to Symbolic evaluation
Bounded model-checking, Case splitting, Rosette solver, State merging, Symbolic execution, Verification performance of code, Verification profiling of code, Verifier performance
Papers related to Symbolic evaluation
- Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
- Software model checking [jhala:compsurv:2009]
- Efficient state merging in symbolic execution [kuznetsov:pldi:2012]
- Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
- Growing solver-aided languages with Rosette [torlak:onward:2013]
- A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]