menu

School of Electronic Engineering and Computer Science

People menu

Pasquale Malacaria, PhD

Pasquale

Professor of Computer Science

Email: p.malacaria@qmul.ac.uk
Telephone: +44 20 7882 6378
Room Number: Peter Landin, CS 428
Website: http://www.eecs.qmul.ac.uk/~pm
Office Hours: Wednesday 13:00-15:00

Teaching

Object-Oriented Programming (Undergraduate)

Major topics include the concepts of class, object, method, subclass, inheritance and their use in programming. The relevance of the object oriented style with respect to concrete software problems will be stressed both in lectures and labs. There will be two hours of lectures per week, and each student will have a weekly timetabled lab session. In addition, you will be expected to spend further time outside scheduled lab periods in the lab (or at home machines if they are available), and to read textbooks and review notes.

Program Specifications (Undergraduate/Postgraduate)

The module will cover: 1. Introduction to Logic for Systems and Program Verification and Analysis 2. Using Hoare Logic: The specification language - describing properties of programs; Proof rules in Hoare logic - verifying properties of programs; Basic technologies behind building automatic program verification tools based on Hoare logic; Using automatic verification tools based on Hoare logic. 3. Introduction to modelchecking and Spin: Temporal logic: modelling states and operations of a system; Modelchecking logics in particular CTL; Safety and Liveness in systems; Using Spin for checking properties and for problem solving.

Software Analysis and Verification (Undergraduate)

Software analysis and verification is about being able to rigorously analyse and verify software. While testing is a very effective way to eliminate software bugs, it cannot guarantee their elimination. Tools based on logics as introduced in ECS715P 'Programme Specifications' are more and more effective in providing strong guarantees in the analysis and verification of software, in particular in the elimination of software bugs.

Software Analysis and Verification (Postgraduate)

The module will cover: 1. Introduction to Logic for Systems and Program Verification and Analysis 2. Using Hoare Logic: The specification language - describing properties of programs; Proof rules in Hoare logic - verifying properties of programs; Basic technologies behind building automatic program verification tools based on Hoare logic; Using automatic verification tools based on Hoare logic. 3. Introduction to modelchecking and Spin: Temporal logic: modelling states and operations of a system; Modelchecking logics in particular CTL; Safety and Liveness in systems; Using Spin for checking properties and for problem solving.

Research

Research Interests:

Information theory and program analysis, computer security, semantics of programming languages

Publications

Return to top