The Blockchain@Unica Lab at the University of Cagliari conducts foundational and applied research on decentralized ledger technologies, with a special focus on programming languages and security. Since 2015 we are a local node of the Cyber Security National Laboratory, and in 2018 we co-founded the Italian Distributed Ledger Technology Working Group.
News
Projects
Current projects:
Past projects:
Publications
2024
- M. Bartoletti, L. Benetollo, M. Bugliesi, S. Crafa, G. Dal Sasso, R. Pettinau, A. Pinna, M. Piras, S. Rossi, S. Salis, A. Spanò, V. Tkachenko, R. Tonelli, R. Zunino. Smart Contract Languages: a comparative analysis
, Future Generation Computer Systems 164, 2024
- M. Bartoletti, R. Marchesin, R. Zunino. Secure compilation of rich smart contracts on poor UTXO blockchains. IEEE European Symposium on Security and Privacy, 2024
- M. Bartoletti, R. Marchesin, R. Zunino. DeFi composability as MEV non-interference. Financial Cryptography, 2024
- M. Bartoletti, F. Fioravanti, G. Matricardi, R. Pettinau and F. Sainas. Towards Benchmarking of Solidity verification tools. FMBC, 2024
- D. Pusceddu and M. Bartoletti. Formalizing Automated Market Makers in the Lean 4 Theorem Prover. FMBC, 2024
- M. Bartoletti, A. Ferrando, E. Lipparini, V. Malvone. Solvent: liquidity verification of smart contracts, iFM, 2024
- M. Bartoletti, R. Marchesin, R. Zunino. Scalable UTXO Smart Contracts via Fine-Grained Distributed State. ArXiV preprint, 2024
2023
2022
- M. Bartoletti, J. Hsin-yu Chiang, A. Lluch-Lafuente. A theory of Automated Market Makers in DeFi (extended version of the equally titled COORDINATION 2021 paper). In Logical Methods in Computer Science 18(4), 2022
- M. Bartoletti, S. Lande, M. Murgia, R. Zunino. Verifying liquidity of recursive Bitcoin contracts. In Logical Methods in Computer Science 18(1), 2022.
- M. Bartoletti, J. Hsin-yu Chiang, A. Lluch-Lafuente. Maximizing Extractable Value from Automated Market Makers. Financial Cryptography, 2022
- M. Bartoletti, M. Murgia, R. Zunino. A Sound Up-to-n,δ Bisimilarity for PCTL. COORDINATION, 2022
- M. Bartoletti, J.H. Chiang, T. Junttila, A. Lluch-Lafuente, M. Mirelli, A. Vandin. Formal Analysis of Lending Pools in Decentralized Finance. ISOLA, 2022
2021
- M. Bartoletti, L. Galletta, M. Murgia. A theory of transaction parallelism in blockchains. In Logical Methods in Computer Science, 17(4), 2021
- M. Bartoletti, S. Lande, A. Loddo, L. Pompianu, S. Serusi. Cryptocurrency scams: analysis and perspectives. IEEE Access, 2021
- M. Bartoletti, J. Hsin-yu Chiang, A. Lluch-Lafuente. A theory of Automated Market Makers in DeFi. COORDINATION, 2021
- M. Bartoletti, S. Lande, R. Zunino. Computationally sound Bitcoin tokens. CSF, 2021
- M. Bartoletti, J. Hsin-yu Chiang, A. Lluch Lafuente. SoK: Lending pools in decentralized finance. WTSC, 2021.
- M. Bartoletti, A. Bracciali, C. Lepore, A. Scalas, R. Zunino. A formal model of Algorand smart contracts. Financial Cryptography, 2021.
- M. Bartoletti, J. Hsin-yu Chiang, A. Lluch-Lafuente. Towards a Theory of Decentralized Finance. DeFi Workshop, 2021.
2020
- M. Bartoletti, S. Carta, T. Cimoli, R. Saia. Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact. In Future Generation Computer Systems, 102, 2020
- M. Bartoletti. Smart contracts contracts. In Frontiers in Blockchain (Perspective article), 2020.
- M. Bartoletti, M. Murgia, R. Zunino. Renegotiation and recursion in Bitcoin contracts. COORDINATION 2020
- M. Bartoletti, L. Galletta, M. Murgia. A true concurrent model of smart contracts executions. COORDINATION, 2020 (Awarded as COORDINATION 2020 best paper and as IFIP Best Paper Award)
- M. Bartoletti, S. Lande, R. Zunino. Bitcoin covenants unchained. ISOLA, 2020
2019
- N. Atzei, M. Bartoletti, S. Lande, N. Yoshida, R. Zunino. Developing secure Bitcoin contracts with BitML. ESEC/FSE, 2019 and Scaling Bitcoin Workshop, 2019.
- M. Bartoletti, B. Bellomy, L. Pompianu. A journey into Bitcoin metadata. Journal of Grid Computing 17(1), 3-22, 2019
- M. Bartoletti, L. Galletta, M. Murgia: A minimal core calculus for Solidity contracts. CBT, 2019
- M. Bartoletti, R. Zunino. Verifying liquidity of Bitcoin contracts. POST, 2019
- M. Bartoletti, R. Zunino. Formal models of Bitcoin contracts: a survey. Frontiers in Blockchain, 2019.
2018
- N. Atzei, M. Bartoletti, T. Cimoli, S. Lande, R. Zunino. SoK: unraveling Bitcoin smart contracts. POST, 2018
- N. Atzei, M. Bartoletti, S. Lande, R. Zunino. A formal model of Bitcoin transactions. Financial Cryptography, 2018
- M. Bartoletti, R. Zunino. BitML: a calculus for Bitcoin smart contracts. ACM CCS, 2018
- M. Bartoletti, T. Cimoli, R. Zunino. Fun with Bitcoin smart contracts. ISOLA, 2018
- M. Bartoletti, T. Cimoli, L. Pompianu, S. Serusi. Blockchain for social good: a quantitative analysis. Goodtechs, 2018
- M. Bartoletti, B. Pes, S. Serusi. Data mining for detecting Bitcoin Ponzi schemes. Crypto Valley Conference on Blockchain Technology, 2018
2017
- N. Atzei, M. Bartoletti, T. Cimoli. A survey of attacks on Ethereum smart contracts (SoK). POST, 2017
- M. Bartoletti, A. Bracciali, S. Lande, L. Pompianu. A general framework for blockchain analytics. SERIAL, 2017
- M. Bartoletti, R. Zunino. Constant-deposit multiparty lotteries on Bitcoin. Bitcoin Workshop, 2017
- M. Bartoletti, L. Pompianu. An analysis of Bitcoin OP_RETURN metadata. Bitcoin Workshop, 2017
- M. Bartoletti, L. Pompianu. An empirical analysis of smart contracts: platforms, applications, and design patterns. WTSC, 2017
- M. Bartoletti, S. Lande, A.S. Podda. A Proof-of-Stake protocol for consensus on Bitcoin subchains. WTSC, 2017
Talks
- MEV-freedom in DeFi and beyond. Invited talk at FMBC 2022
- Maximizing Extractable Value from Automated Market Makers talk at Financial Cryptography, 2022
- Smart contracts in Bitcoin and BitML. Invited talk at the 3rd Workshop on Blockchain-based Architectures (BlockArch), 2022
- Formal methods for DeFi - Lending Pools and beyond. Invited talk at NYU Stern Fintech Conference, 2022
- Smart contracts in Bitcoin and BitML talk at Dagstuhl Seminar on Rigorous Methods for Smart Contracts, 2021
- A formal model of Algorand smart contracts talk at TPBC, 2021
- A formal model of Algorand smart contracts talk at Financial Cryptography, 2021
- Computationally sound Bitcoin tokens talk at Computer Security Foundations, 2021
- Bitcoin covenants unchained talk at ISOLA, 2020
- A true concurrent model of smart contracts executions talk at COORDINATION, 2020
- Renegotiation and Recursion in Bitcoin Contracts talk at COORDINATION, 2020
- Developing secure contracts with BitML talk at Scaling Bitcoin Workshop, 2019
- BitML tool demo talk at ESEC/FSE, 2019
- BitML: a calculus for Bitcoin smart contracts talk at ACM CCS, 2018