The scope of the present project is the verification of properties of safety-critical software. Our approach will focus simultaneously on two techniques: software model checking and deductive reasoning, both advancing the state of the art at the theoretical level and producing tools that can be used by companies developing critical applications. We are particularly interested in interactions between both approaches, which have historically fed back into each other.

One particular topic that will be investigated is the formal verification of shared memory concurrent programs, elucidating the feasibility of their use in the safety-critical context.