Currently active RESCUE-related research opportunities (at the undergraduate and post-graduate levels) are announced here.

PhD Opportunities

• Domain-specific Program Verification Infrastructures: proposed by JoseBacelarAlmeida and JorgeSousaPinto in the context of the MAPi doctoral programme.

Master Opportunities

Automated Model checking in ADA/Spark Topic: Model checking for real-time systems allows to ensure that a system (the model) verifies the required temporal properties. To be useful, the model must be automatically inferred/translated from the system source code. In the scope of the RESCUE project, it was developed a translation from HTL (a coordination language for concurrent real-time systems) to timed-automata networks of the UPPAAL system. Based on this experience, it is intended to extend/adapt this framework To the ADA/Spark language. The work will include the construction of a translator able to abstract ADA tasks coordination and provide a model for which temporal properties can be analysed.

Call closes on November 12, 2009. To apply see www.eracareers.pt.

For more information contact nam@ncc.up.pt or desousa@di.ubi.pt.

Research Training Opportunities

• bolsaRescue0909.pdf: ADA/SPARK model checking