During this secondment we worked on the usage of behavioural descriptions for the static analysis of smart contracts. The goal is to combine the tools and techniques previously developed by NOVA and UBA for the analysis of programs in this application domain. During the secondment, we have identified the main challenges (i.e., adapt the techniques to this application domain, develop a formal model for smart contract languages) and explore ideas to combine approaches.
This secondment was related to Tasks T.4.2 & T.4.4 – (O.4.2 & O.4.3).