We present a technique for verifying concurrent software systems via SAT-based three-valued bounded model checking. It is based on a direct transfer of the system to be analysed and a temporal logic property into a ...