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.