COPLAS: Albert, Superoptimization of (Optimized) Smart Contracts

On 7 December, Elvira AlbertComplutense University of Madrid, Spain, will give a talk about the Superoptimization of Smart Contracts.


Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence.  This talks overviews our approach for super-optimization of smart contracts based on Max-SMT which is split into two main phases: (i) the extraction of a functional specification from the basic blocks of the smart contract, which is simplified using rules that capture the semantics of the arithmetic, bit-wise, relational operations, etc. and (ii) the synthesis of optimized blocks which, by means of an efficient Max-SMT encoding, finds the bytecode blocks with minimal cost (according to the selected optimization criteria) and whose functional specification is equal (modulo commutativity) to the extracted one.  Our experiments on randomly selected real contracts achieve important gains in gas and in bytes-size over code already optimized by solc.


Elvira is professor at Complutense University of Madrid.  See for more information.

See also


All are welcome. No registration required.  Feel free to forward this invitation.

To be informed about Copenhagen Programming Languages Seminar (COPLAS) and related talks, visit  If you are interested in joining the (open) Decentralized Systems Group at DIKU, please contact Fritz Henglein.