| Title |
Formalizing IOTA extended UTXO in Isabelle / |
| Authors |
Dlugauskas, Edvardas ; Petrauskas, Karolis |
| DOI |
10.15388/LMITT.2024.3 |
| Full Text |
|
| Is Part of |
Lietuvos magistrantų informatikos ir IT tyrimai: konferencijos darbai, 2024 m. gegužės 10 d... Vilnius : Vilniaus universiteto leidykla. 2024, p. 26-35.. eISSN 2783-784X |
| Keywords [eng] |
IOTA ; UTXO model ; EUTXO model ; formal verification ; Isabelle ; formal methods |
| Abstract [eng] |
The IOTA Extended UTXO (IOTA EUTXO) model extends the UTXO blockchain to include features like smart contracts and non-fungible tokens. In this work, we show that the IOTA EUTXO model maintains the base correctness properties of the UTXO model while extending it with extra functionality. We achieve this by specifying and verifying the essential concepts of the base UTXO model and the extensions proposed by IOTA using the Isabelle proof assistant. The specification is designed to be modular and extensible, meaning it can be used as a foundation for further research of the UTXO and IOTA EUTXO models. |
| Published |
Vilnius : Vilniaus universiteto leidykla |
| Type |
Conference paper |
| Language |
English |
| Publication date |
2024 |
| CC license |
|
