José Creissac Campos - Research Positions

Research positions

Post-doc positions

If you are interested in some of these topics do contact me!

Tools for the formal verification of critical interactive systems through model checking and theorem proving: This position is offered in the context of the ON.2 SR&TD Integrated Program "BEST CASE - Better Science Through Cooperative Advanced Synergetic Efforts", supported by the Programa Operacional Regional do Norte (ON.2). See reference BPD-2013_BestCase_RL8.1_UMINHO in this call.
The role of different verification tools - software model checkers, timed model checkers, theorem provers - in the verification of real time software: This position is offered in the context of the ON.2 SR&TD Integrated Program "BEST CASE - Better Science Through Cooperative Advanced Synergetic Efforts", supported by the Programa Operacional Regional do Norte (ON.2). See reference BPD-2013_BestCase_RL8.2_UMINHO in this call.

PhD studentships

If you are interested in some of these topics do contact me!
Se also the MSc themes below. Most of them can also be extended to PhDs.

Interactive Computing Systems' Reliability Analysis

This research theme follows from an ongoing effort to develop tools and techniques for the systematics analysis of interactive systems' designs. The basic building blocks of the verification approach have been defined, and tool support developed. The goal of the current proposal is to broaden the scope of the approach. We are interested in highly moded interfaces, which pose particular challenges in terms of modelling, and in exploring how the approach can be applied in complex interactive computing applications. (see more...)

This studenship is offered in the context of the ON.2 SR&TD Integrated Program "BEST CASE - Better Science Through Cooperative Advanced Synergetic Efforts", supported by the Programa Operacional Regional do Norte (ON.2). See reference BIM-2013_BestCase_RL8.1_UMINHO in this call.

MSc themes

If you are interested in some of these topics do contact me!
Most of these topics can be extended to PhDs.

Desenvolvimento de um ambiente de geração e execução de casos de teste

Os testes de software, em particular da camada de interface, são cruciais para garantir a qualidade do software. No entanto, o processo de teste tende a ser demorado e caro em termos de recursos. Os testes baseados em modelos (model-based testing) permitem automatizar o processo de teste comparando o sistema implementado com um modelo do sistema (o oráculo). Para tal, a partir do oráculo são gerados casos de teste (sequências de acções) a executar tanto na implementação como no modelo. No caso da camada de interface, no entanto, um oráculo tipico considera apenas o comportamento esperado do utilizador, não detectando por isso problemas que possam acontecer devido a erros de utilização.

Com este projecto pretende-se desenvolver uma ferramenta capaz de gerar e executar mutações de casos de teste, de modo a testar o comportamento da aplicação em caso de erros de utilização. Deste modo será possível melhorar a capacidade de detecção de erros deste tipo de técnica e aumentar a garantia de qualidade que a técnica permite.

Esta proposta insere-se no projecto PBGT, existindo possibilidade de financiamento.