1. A computer-implemented method for symbolic execution of executable code using parametric states, comprising: identifying shared state elements and different state elements in execution states associated with the executable code; representing the different state elements using a state abstraction; based on the state abstraction, defining a parametric state having a parametric constraint, the parametric state losslessly representing a group of the execution states, wherein an execution state in the group of execution states is an instance of the parametric state; and symbolically executing the executable code using a processor having access to memory media, including using the parametric state.