menu

School of Electronic Engineering and Computer Science

People menu

Mr Arthur Passos De Rezende

Arthur

Email: a.passosderezende@qmul.ac.uk
Room Number: Peter Landin, CS 429

Teaching

Program Specifications (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

Return to top