Research Results
IMDEA Software Institute researcher, Manuel Hermenegildo, gives the Opening Invited Talk at the 27th Static Analysis Symposium (SAS'20), on “Cost Analysis of Smart Contracts via Parametric Resource Analysis,” work co-authored with Víctor Pérez, Maximiliano Klemen, Pedro López and José Francisco Morales.
This line of research is motivated by the fact that, in blockchains, contract execution and storage are replicated across large numbers of nodes, and this makes resource consumption an important concern. The few cost analyzers that exist for smart contracts are for specific platforms and languages. However, blockchain platforms present significant variability, also over time.
Parametric Resource Analysis (also referred to as User-Defined Resource Analysis) is a generic approach, proposed by the IMDEA Software Institute team, for developing analyzers that infer safe bounds on different resources and with different resource models. In the talk, Manuel Hermenegildo reviews this approach and explores its application to the static inference of gas and storage consumption bounds for smart contracts, reporting on a concrete case study: developing an analyzer for the Tezos platform and its Michelson language. The results show that the approach is an effective method for the rapid development and maintenance of cost analyzers for smart contracts.
The Parametric Resource Analysis approach was awarded the 10 year Test-of-Time Award at the 2017 International Conference on Logic Programming, the premier conference in the area.
IMDEA Software’s CiaoPP framework implements this approach and allows its application to different programming languages, by translation into a Horn clause-based intermediate representation.
The series of International Static Analysis Symposia (SAS) serves as the primary venue for presentation of theoretical, practical, and application advances in this area. This edition of SAS is co-located with SPLASH'20 in an online form, coordinated from Chicago, USA, from November 18 to November 20, 2020. SPLASH embraces all aspects of software construction and delivery, to make it the premier conference on the applications of programming languages - at the intersection of programming languages and software engineering.
The associated work is conducted in the context of the collaboration of the Tezos foundation and Nomadic labs with the IMDEA Software Institute.
