Bisimulation Algorithmics (available)

Labelled transition systems are a crucial abstraction to understandcomplex and distributed systems. Bisimulation, in its many variations,is conceptually at the core of many verification tools. One such toolis OvenMPST. OvenMPST is a tool for validatingand handling multiparty protocol specifications. In this tool,bisimulation plays a central role in establishing that a protocol iswell formed and correctly … full description “Bisimulation Algorithmics (available)”

Building a Full Causality Chain Across an Enterprise System (completed)

Data Provenance refers to records of the inputs, entities, systems and process that influence data of interest, providing a historical record of the data and its origins. To provide a holistic view of the data provenance in an enterprise system, the provenance records of the activities carried out on a client workstation is important. Last … full description “Building a Full Causality Chain Across an Enterprise System (completed)”

Empirical evaluation of static verifiers for the Go programming language (available)

Go is a language that natively supports many constructs to synchronise concurrent threads. Because of this, developing code that contains subtle concurrency bugs is rather common. To address this problem, several groups of researchers have put forwards tools to find concurrency bugs in Go codebases. The objective of this project is to evaluate how some … full description “Empirical evaluation of static verifiers for the Go programming language (available)”

Formal Verification for Blockchains (available)

In this project you will explore the world of formal verification andblockchains, specifically the new Ethereum 2.0 ‘Proof-of-Stake’ blockchain [1]. This is a more energy-efficient replacement for the original Ethereum ‘Proof-of-Work’ blockchain. As in any blockchain, correctness of thedistributed ‘consensus’ protocol [2] used to maintain the chain and extend it with new blocks is critical. … full description “Formal Verification for Blockchains (available)”

Jupyter notebooks (available)

  Prerequisites: experience with Python (useful) and Javascriptprogramming (essential). It may be useful to be willing to learn aboutfunctional programming (but this is not essential). Jupyter notebooks [1] are examples of literate programming [2] wherecode and outputs from the code as well as documentation are in the sameapplication. Jupyter allows the user to run code … full description “Jupyter notebooks (available)”