• Gordon Pace (gordon.pace@um.edu.mt)
  Formal methods for software and hardware design, compositional verification, synchronous languages and semantics of programming languages.
  Currently working on hybrid system verification, compositional verification techniques for model-checking asynchronous systems and the use of embedded languages for synchronous system design and refinement.

• Adrian Francalanza (adrian.francalanza@um.edu.mt)
  Operational semantics and type systems. The Pi-calculus, its variants and other process calculi, with specific focus on failure and resource management within such formalisms. Also interested in algorithms for asynchronous distributed settings and how these address issues such as partial failure and resource constraints. The formal specification and correct construction of compilers together with more practical aspects such as compiler optimisations and intermediate code generation.

• Christian Colombo (christian.colombo@um.edu.mt)
  Large-scale industrial systems are not always resilient to the impact of runtime verification. The challenge is to find ways in which verification is performed without intruding in the normal operation of a system while at the same time being able to take compensating actions which mitigate the problem found. The approach being considered is to perform verification on a separate machine and execute compensating actions within an acceptable time period after the problem has occurred. This makes the impact of verification much smaller than pure runtime verification.

• Joseph Cordina (joseph.cordina@um.edu.mt)
  Automatic verification of hardware and semi-hardware systems mainly concentrating on sychronous and reactive systems. Currently working on the use of embedded language for hardware compiler verification using a selection of techniques such as induction on the structure of the compilation process.

• Ingram Bondin
  

• Adrew Gauci
  

• Kevin Falzon
  

• Andrew Calleja
  Scripting of artificial intelligence in games is often quite done in a domain-specific language, replicating much of standard programming language features. In this manner, programs which control the AI are fixed sequences of instructions following a set of steps while attempting to mimic human behaviour. We are looking into an alternative approach of using the techniques from the embedded language community to build an embedded domain-specific language for AI scripting for certain games. In this manner, AI scripts become data objects in the programming host language, enabling parametrised strategies, and manipulation of the strategies directly through programs in the host programming language.
  This will enable the creation of adaptive two-stage scripts: (i) fixed strategies in the AI language; and (ii) programs in the host language enabling the modification and adaptation of the scripts in the domain specific language to react to the state of the game. Embedded language techniques give us precisely the power required to create such a scripting language for adaptive AI.

• Ruth Schembri
  Software development lifecycles need to be flexible enough to cater for changes in specifications, whilst also aiming for the fastest possible delivery of software products. Meanwhile, software systems are constantly attempting to offer increasingly more functionality and incorporated fault-tolerance.
  Runtime verification and refinement are two techniques which can be used to verify the correctness of systems. It is possible to monitor the execution of a system to ensure that this conforms to a given specification using runtime verification. Meanwhile, refinement characterises the changes in a specification over successive levels in the development lifecycle, by which it evolves into a concrete design or implementation.
  This project aims to exploit both these techniques in order to create a verification mechanism by which a system can be monitored after release, with the ability to detect system malfunction with respect to specifications from any level of abstraction, and to detect inconsistencies in the specifications. evolution over the development cycle, by identifying execution traces for which a refinement relation between two levels does not hold.

• Mark Bonnici
  
• Christian Tabone
  
• Stephen Fenech
  
• Christian Colombo
  
• Karlston Demanuele
  
• Christine Vella
  

We are always on the lookout for good students. If you are interested in doing an MSc or PhD in an area of interest to SVRG, just get in touch. Also, if you'd like to visit and give a talk, please do not hesitate to contact us.