{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,9]],"date-time":"2025-05-09T18:25:40Z","timestamp":1746815140413,"version":"3.28.0"},"reference-count":15,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T00:00:00Z","timestamp":1682899200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,5,1]]},"DOI":"10.1109\/icbc56567.2023.10174901","type":"proceedings-article","created":{"date-parts":[[2023,7,12]],"date-time":"2023-07-12T17:20:50Z","timestamp":1689182450000},"page":"1-9","source":"Crossref","is-referenced-by-count":5,"title":["Djed: A Formally Verified Crypto-Backed Autonomous Stablecoin Protocol"],"prefix":"10.1109","author":[{"given":"Joachim","family":"Zahnentferner","sequence":"first","affiliation":[{"name":"Djed Alliance,Brazil"}]},{"given":"Dmytro","family":"Kaidalov","sequence":"additional","affiliation":[{"name":"Input Output,Ukraine"}]},{"given":"Jean-Fr\u00e9d\u00e9ric","family":"Etienne","sequence":"additional","affiliation":[{"name":"Input Output,France"}]},{"given":"Javier","family":"D\u00edaz","sequence":"additional","affiliation":[{"name":"Input Output and Atix Labs,Argentina"}]}],"member":"263","reference":[{"journal-title":"A Note on Cryptocurrency Stabilisation Seigniorage Shares","year":"2014","author":"sams","key":"ref13"},{"key":"ref12","first-page":"112","article-title":"Utxosfma: UTXO with multi-asset support","volume":"12478","author":"chakravarty","year":"0","journal-title":"Leveraging Applications of Formal Methods Verification and Validation Applications - 9th International Symposium on Leveraging Applications of Formal Methods ISoLA 2020 Rhodes Greece October 20&#x2013;30 2020 Proceedings Part III ser Lecture Notes in Computer Science"},{"journal-title":"statiCoin and riskCoin","year":"2017","author":"edge","key":"ref15"},{"journal-title":"The Maker protocol MakerDAO's multi-collateral Dai (MCD) system","year":"2017","key":"ref14"},{"key":"ref11","article-title":"Multi-Currency Ledgers","author":"zahnentferner","year":"2020","journal-title":"Cryptology ePrint Archive Report"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_10"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"ref1","first-page":"510","article-title":"The Kind 2 Model Checker","author":"champion","year":"2016","journal-title":"Computer Aided Verification"},{"journal-title":"The Plutus Platform","year":"0","key":"ref8"},{"key":"ref7","article-title":"Djed: A formally verified crypto-backed pegged algorithmic stablecoin","author":"zahnentferner","year":"2021","journal-title":"Cryptology ePrint Archive Report"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/978-3-030-33636-3_15","article-title":"Unraveling Recursion: Compiling an IR with Recursion to System F","volume":"11825","author":"jones","year":"0","journal-title":"Mathematics of Program Construction - 13th International Conference MPC 2019 Porto Portugal October 7&#x2013;9 2019 Proceedings ser Lecture Notes in Computer Science"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"ref3","first-page":"457","article-title":"Bounded Model Checking","volume":"185","author":"biere","year":"2009","journal-title":"Handbook of Satisfiability Ser Frontiers in Artificial Intelligence and Applications"},{"key":"ref6","volume":"2283","author":"nipkow","year":"2002","journal-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic Ser LNCS"},{"key":"ref5","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","author":"paulson","year":"1994","journal-title":"Isabelle A Generic Theorem Prover ser Lecture Notes in Computer Science"}],"event":{"name":"2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)","start":{"date-parts":[[2023,5,1]]},"location":"Dubai, United Arab Emirates","end":{"date-parts":[[2023,5,5]]}},"container-title":["2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10174862\/10174863\/10174901.pdf?arnumber=10174901","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,1]],"date-time":"2023-08-01T17:57:12Z","timestamp":1690912632000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10174901\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,1]]},"references-count":15,"URL":"https:\/\/doi.org\/10.1109\/icbc56567.2023.10174901","relation":{},"subject":[],"published":{"date-parts":[[2023,5,1]]}}}