Analysis and Verification of Critical Concurrent Programs
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.
(
read more)
Project info
| Este trabalho é financiado por Fundos FEDER através do Programa Operacional Fatores de Competitividade - COMPETE e por Fundos Nacionais através da FCT - Fundação para a Ciência e a Tecnologia no âmbito do projeto FCOMP-01-0124-FEDER-020486 |
| This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020486 |
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.