Presented as part of the 2013 HCSS conference.
ABSTRACT
Symbolic simulation is a powerful technique for building mathematical models describing a program's results by simulating execution while interpreting inputs as symbolic variables. Such models can then be used to prove properties about the corresponding source program, including equivalence against a reference implementation.
