View Proposal
-
Proposer
-
Andrew Ireland
-
Title
-
PlusCal: A language for writing and verifying concurrent (multi-threaded) algorithms
-
Goal
-
Develop teaching materials for the PlusCal.
-
Description
- PlusCal is a language for writing concurrent (multi-threaded) algorithms. It compiles to a formalism called TLA+, where verification is supported via model checking, i.e., safety, liveness and temporal properties. TLA+ and its associated tools are used in industry, for example, AWS, Microsoft and Intel. Through an in-depth study, the aim of this project is to develop teaching materials that provide an introduction to PlusCal and TLA+ that highlights both its strengths and limitations.
- Resources
-
https://lamport.azurewebsites.net/tla/tutorial/intro.html
-
Background
-
Ideally F20RS
-
Url
-
External Link
-
Difficulty Level
-
Challenging
-
Ethical Approval
-
None
-
Number Of Students
-
-2
-
Supervisor
-
Andrew Ireland
-
Keywords
-
software engineering, concurrency, multi-threaded applications, formal verification, model checking
-
Degrees
-
Master of Engineering in Software Engineering