In his master thesis Vladimir Herdt presents a novel approach called complete symbolic
simulation for a more efficient verification of much larger (non-terminating) SystemC
programs. The approach combines symbolic simulation with stateful model checking and allows to
verify safety properties in (cyclic) finite state spaces by exhaustive exploration of all
possible inputs and process schedulings. The state explosion problem is alleviated by
integrating two complementary reduction techniques. Compared to existing approaches the
complete symbolic simulation works more efficiently and therefore can provide correctness
proofs for larger systems which is one of the most challenging tasks due to the ever
increasing complexity.
