{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:48:16Z","timestamp":1767340096939,"version":"3.28.0"},"reference-count":14,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,5,2]],"date-time":"2022-05-02T00:00:00Z","timestamp":1651449600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,5,2]],"date-time":"2022-05-02T00:00:00Z","timestamp":1651449600000},"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":[[2022,5,2]]},"DOI":"10.1109\/icbc54727.2022.9805487","type":"proceedings-article","created":{"date-parts":[[2022,6,29]],"date-time":"2022-06-29T19:46:19Z","timestamp":1656531979000},"page":"1-3","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Payment Channels with TLA<sup>+<\/sup>"],"prefix":"10.1109","author":[{"given":"Matthias","family":"Grundmann","sequence":"first","affiliation":[{"name":"Institute of Information Security and Dependability (KASTEL) Karlsruhe Institute of Technology (KIT),Karlsruhe,Germany"}]},{"given":"Hannes","family":"Hartenstein","sequence":"additional","affiliation":[{"name":"Institute of Information Security and Dependability (KASTEL) Karlsruhe Institute of Technology (KIT),Karlsruhe,Germany"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1109\/CSF49147.2020.00031"},{"year":"2021","journal-title":"Lightning network specifications","key":"ref11"},{"year":"2021","author":"grundmann","journal-title":"Specification of Protocol for Payment Channel in TLA+","key":"ref12"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1007\/978-3-030-66172-4_26"},{"year":"2022","author":"grundmann","journal-title":"Exemplary Output of Visualization of Counterexamples","key":"ref14"},{"year":"2021","journal-title":"The TLA Toolbox","key":"ref4"},{"year":"2002","author":"lamport","journal-title":"Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers","key":"ref3"},{"year":"2020","author":"close","article-title":"Breaking state channels with TLA+","key":"ref6"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.1145\/3360549"},{"key":"ref8","first-page":"10:1","article-title":"Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)","volume":"84","author":"braithwaite","year":"0"},{"key":"ref7","article-title":"Quartz: A Framework for Engineering Secure Smart Contracts","author":"kolb","year":"2020","journal-title":"EECS Department University of California Berkeley Tech Rep UCB\/EECS-2020-178"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1145\/177492.177726"},{"key":"ref1","article-title":"The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments","author":"poon","year":"2016","journal-title":"Tech Rep"},{"doi-asserted-by":"publisher","key":"ref9","DOI":"10.1145\/3491003.3491006"}],"event":{"name":"2022 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)","start":{"date-parts":[[2022,5,2]]},"location":"Shanghai, China","end":{"date-parts":[[2022,5,5]]}},"container-title":["2022 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9805458\/9805482\/09805487.pdf?arnumber=9805487","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,25]],"date-time":"2022-07-25T20:14:05Z","timestamp":1658780045000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9805487\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,2]]},"references-count":14,"URL":"https:\/\/doi.org\/10.1109\/icbc54727.2022.9805487","relation":{},"subject":[],"published":{"date-parts":[[2022,5,2]]}}}