A new verification project has recently started at Philips Research. It concerns verification of C-like concurrent programs
used to specify functionality of hardware-software systems. The problem is to make the verification practical, in the sense
that it must be mechanized, and applicable to thousands of lines of C-like code. We present the goals of the project and some
combination of existing solutions we want to try.