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)”
Supervisor: Francisco Ferreira
Active: updated 2-AUG-2022 (OSAA035) no expiry
Correct and Certified Regular Expressions (completed)
In programming language research ideas are explored in an ofte repeated loop. You have an idea then propose the language feature to study, its semantics, and the prove it has the properties you expect (type safety, performance, expressivity, etc.). In this project, we want to explore such a cycle working with regular expressions as the … full description “Correct and Certified Regular Expressions (completed)”
Embedded firmware development for the Open Bot Brain project (available)
Software is a vital part of our infrastructure. You may be familiarwith software running on computers and phones. But software runs onmany more devices as part of an embedded microcontroller in thedevice, software running on embedded devices is often called firmware.Examples range from toothbrushes, to appliances, to tools, and devicesin the so called internet of … full description “Embedded firmware development for the Open Bot Brain project (available)”