Central to all SMC techniques is the notion of equivalence classes of execution sequences. To ensure soundness of verification an SMC technique must explore at least one sequence per equivalence class. Most existing techniques rely on a fine notion of equivalence based on conflicting memory accesses.
There is a recent interest from the community in designing coarser notions of equialence to make SMC scalable while preserving soundness. In this talk I will introduce one such coarser notion based on values. I will be discussing the significance of the same and presenting an SMC technique based on the proposed notion of equivalence.