During this secondment I worked with Dr Antonio Ravara and Dr Hernan Melgratti in application of behavioural description to the static analysis of Smart Contracts. To do so, we deeply study the state of the art and the practice of the area, including works on BitCoin, Tezos, Zilliqa networks.
We focused mainly in aspect aspects: i) mechanisms to formalize low level languages and virtual machines executing in the blockchain environment, ii) formalizations of consensus protocols on the blockchain ecosystems, iii) high level languages to write smart contracts and they formal underpinnings, iv) static analysis technique to enforce security properties. We analyzed the advances in those areas and the current limitations and challenges. The next steps are the introduction of session types to a core language and formalize its semantics in a machine provable language like Coq.
I also worked on the preparation of the tutorial on Abstractions for Validating and Testing APIs that I will present in the BeHAPI summer school in Leicester.