From simulation to verification (and back)

Symbolic evaluation is the execution of software and software designs on inputs given as symbolic or explicit constants along with constraints on these inputs. Efficient symbolic evaluation is now feasible due to recent advances in efficient decision procedures and symbolic model checking. Symbolic evaluation can be applied to partially implemented descriptions and provides wider coverage and greater assurance than testing and traditional simulation alone. Unlike full formal verification, symbolic evaluation can be used in a partial manner that is more likely to succeed and yield some degree of assurance. Its main advantage is that it can be used within a smooth spectrum of analyses ranging from refutation based on explicit-state simulation to full-blown verification.