In page 4 at the last line they define it as:
LASER-Ethereum is a symbolic interpreter for Ethereum bytecode.
Given one or more smart contract accounts as input, it returns a set
of abstract program states. A state consists of the set of values
that the virtual machine variables (such as the program counter,
virtual machine stack, and account balances) take at a particular
point during execution.
And in the github website: https://github.com/b-mueller/laser-ethereum. They say it is a:
LASER is a symbolic virtual machine (SVM) that runs Ethereum smart
contracts. It accurately models most features of the Ethereum virtual
machine including inter-contracts calls.
it helps you know with this if it run into the problem, it can give you the certain input and the trace for you reproduce it. So you don’t need to waste a lot of time to try every random input
To understand about symbolic execution you can follow
disclaimer: i haven’t used this but according to what i read and research about it for 1 hour this is what i can do. If you see anything that is wrong please tell me.