Sabine Broda
Completed
About
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.
Research Group
Duration
36months
Start Date
Internal Members
Useful Links
Partners
Universidade do Minho