Automated counter-example guided correction of Promela models violating ω-regular properties.
- Translating (Solidity) Smart Contracts to Promela and Performing Model Checking
The goal is to perform formal verification on the blockchain. One of the most powerful and most widely used model checkers is SPIN. SPIN performs model checking on models written in PROMELA.
The task is to develop a Solidity to PROMELA translator, so that smart contracts can be converted to PROMELA models and thereafter formally verified. Appropriate properties will also have to be indetified to verify against.
- Simplification of variable evaluation-based guards
Simplifying and unifying a large number of condition evaluations of the form (x == y && a == b && p == q && …) into fewer and shorter conditions that achieve the same effect. This tool will also be incorporated into Protictor as a module.
- PROMELA Parser
Developing a parser for Promela on llvm