Advanced Module : Logics and Languages for Software Reliability and Security
• Reference: EMCL-A-LLSRS
• Courses:
• SCV - Software Construction and Verification
• MVCS - Modelling and Validation of Concurrent Systems
• Requirements:
To obtain the 12 crs of the module, students should obtain 6 crs in each of the two courses.
• Description:
The production of software for complex applications, in particular those involving concurrency and security, in which programming errors have serious consequences, has seen some success in the application of formal verification techniques based on model reasoning to establish the correctness of the software.
The purpose of the course is to give an introduction to those techniques. This module is composed by two courses, one focusing on Languages and Models for Concurrency and Security, and other on Logics for Specification and Verification. The first course focuses on principles, methods, techniques and tools for the dependable and trustworthy construction and validation of software systems, ensuring as much as possible the absence of programming errors. The second course focuses on basic principles, techniques, and some tools to help on the challenging task of developing concurrent software systems.
-------------------------------------
SCV - Software Construction and Verification
• Reference: 11159
• Semester: Spring
• Web Page:
• Lecturers: Luís Caires
• Description:
The course covers principles, methods, techniques and tools for the dependable and trustworthy construction and validation of software systems, ensuring as much as possible the absence of programming errors ("bugs"), with a focus on CONCURRENCY and SAFETY.
We will use advanced tools, such as those made available by Microsoft Research in the site http://rise4fun.com and Facebook (INFER), and used by major software companies such as Microsoft, Amazon and Facebook.
This course is a must for all students that wish to master advanced software construction techniques, in particular for concurrent and safe software, an important professional asset.
By the end of the course, students will be able to clearly reason about the correction and safety of developed software, to use sophisticated software analysis tools, to develop and interpret test suites and to write concurrent software.
The course basic language is Java, but we will also use other programmung languages and tools (e.g., JAVASCRIPT, DAFNY, INFER).
-------------------------------------
MVCS - Modelling and Validation of Concurrent Systems
• Reference: 11560
• Semester: Autumn
• Web Page:
• Lecturers: Luís Caires and António Ravara
• Description:
Concurrent and distributed software is nowadays pervasive to most computing devices. However, it is particularly difficult to design and validate. Concurrency bugs appear frequently and have a substantial impact, as not only they may affect many people, but also may cause a severe financial damage. There is thus a pressing need of using rigorous approaches and tools to specify and verify such systems. Industrial actors like Amazon, Facebook, Google, IBM, Intel, Microsoft, or NASA, just to name a few, are using tools to formally guarantee that (parts of) their software is bug-free.
This course covers basic principles, techniques, and some tools to help on the challenging task of developing concurrent software systems. This involves understanding languages to specify systems and their properties. There are various kind of key properties of concurrent systems; we will focus on basic safety and liveness properties, which are enough to express functional requirements of concurrent and distributed algorithms. As basic frameworks, we will explore behavioural models such as automata and transition systems, and state-based models such as the TLA (Temporal Logic of Actions), an approach developed by Lamport. Properties such as deadlock absence or progress can be expressed using specialised logics and automatically checked on tools like TLA+ using model-checking. The modelling and verification techniques covered in this course are used in the design of high assurance systems, or just in large-scale systems where bugs can affect many users.
