The C/C++ 2011 ISO standard (C11) supports relaxed memory consistency with additional ordering constraints over concurrent memory accesses. The C11 semantics, while facilitating compiler optimizations, complicate the reasoning of parallel programs. I will be presenting an efficient stateless model checker for analyzing all relevant C11 program behaviors to detect races on non-atomic variables and safety property violations. I will also introduce a comprehensive HB relation for C11 and a predicate for ‘observational equivalence’, plugged in a partial order reduction algorithm.