Analysis and Verification of Critical Concurrent Programs

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

Supported by
  under contract PTDC/EIA-CCO/108995/2008 (94 KEuro)
Start Date 01 May 2012
Duration 3 years
Hosted by HASLab, Departamento de Informática, Universidade do Minho
Coordination Jorge Sousa Pinto (jsp@di.uminho.pt)
Telefone +351 253604455
Fax +351 253604471

r10 - 22 Apr 2014 - 15:30:07 - JorgeSousaPinto
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM