Ocelot
This project aim to design a declarative programming language for implementing smart contracts and specifying contract-level properties. Driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints, we models each smart contract as a set of relational tables that store transaction records. This relational representation of smart contracts enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance. Specifically, a program consists of a set of declarative rules and violation query rules over the relational representation, describing the smart contract implementation and contract-level properties, respectively. We develop a tool that can compile Decon programs into executable Solidity programs, with instrumentation for run-time property monitoring. We further extends declarative smart contract specifications and applies a set of optimization techniques to automatically generate gas-efficient contract implementations
Publications
- Haoxian Chen, Gerald Whitters, Mohammad Javad Amiri, Yuepeng Wang, Boon Thau Loo. “Declarative Smart Contracts.” The ACM Joint European Software Engineeting Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2022.
People
Lan Lu
Haoxian Chen
Boon Thau Loo
