|
The Semantics & Verification Research Group focuses on the mathematical foundations of computer science, with a particular interest in the analysis and verification of software and hardware. Safety-Critical systems are ones in which errors can be disastrous: loss of life, major financial losses, etc. Techniques to safeguard against such scenarios are essential for such systems, and while testing of systems can identify problems, especially if done in a rigorous fashion. Formal methods, on the other hand, offer techniques ranging from the description of requirements in a formal notation to allow for rigorous reasoning about them, to techniques for automatic verification of hardware and software. The group's research interests include hardware design and verification, software verification, model-checking, synchronous programming, process calculi.
|
Current Members:
-
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.
Masters Students:
Former Masters Students:
- Tyrone Zerafa
- Gabriel Dimech
- Joseph Masini
- Erica Tanti
- Aimee Borda
- Clare Cini
- Ruth Mizzi
- Aldrin Seychell
- Mandy Zammit
- Ingram Bondin
- Kevin Falzon
- Andrew Gauci
- Andrew Calleja
- Ruth Schembri
- Mark Bonnici
- Christian Tabone
- Stephen Fenech
- Christian Colombo
- Karlston Demanuele
- Christine Vella
Are you interested in joining us or visiting the group?
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.
|
|