{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T18:50:47Z","timestamp":1773773447980,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030415990","type":"print"},{"value":"9783030416003","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-41600-3_7","type":"book-chapter","created":{"date-parts":[[2020,3,13]],"date-time":"2020-03-13T05:32:04Z","timestamp":1584077524000},"page":"87-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":45,"title":["Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain"],"prefix":"10.1007","author":[{"given":"Yuepeng","family":"Wang","sequence":"first","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]},{"given":"Shuo","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Rong","family":"Pan","sequence":"additional","affiliation":[]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[]},{"given":"Cody","family":"Born","sequence":"additional","affiliation":[]},{"given":"Immad","family":"Naseer","sequence":"additional","affiliation":[]},{"given":"Kostas","family":"Ferles","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,3,14]]},"reference":[{"key":"7_CR1","unstructured":"Explaining the DAO exploit for beginners in solidity (2016). https:\/\/medium.com\/@MyPaoG\/explaining-the-dao-exploit-for-beginners-in-solidity-80ee84f0d470"},{"key":"7_CR2","unstructured":"Solidity: Function modifiers (2016). https:\/\/solidity.readthedocs.io\/en\/v0.4.24\/structure-of-a-contract.html#function-modifiers"},{"key":"7_CR3","unstructured":"Forecast: Blockchain business value, worldwide, 2017\u20132030 (2017). https:\/\/www.gartner.com\/en\/documents\/3627117"},{"key":"7_CR4","unstructured":"Microsoft azure blockchain (2017). https:\/\/azure.microsoft.com\/en-us\/solutions\/blockchain\/"},{"key":"7_CR5","unstructured":"Parity: The bug that put \\$169m of ethereum on ice? Yeah, it was on the todo list for months (2017). https:\/\/www.theregister.co.uk\/2017\/11\/16\/parity_flaw_not_fixed"},{"key":"7_CR6","unstructured":"Applications and smart contract samples for workbench (2018). https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples"},{"key":"7_CR7","unstructured":"Asset transfer sample for azure blockchain workbench (2018). https:\/\/github.com\/Azure-Samples\/blockchain\/tree\/master\/blockchain-workbench\/application-and-smart-contract-samples\/asset-transfer"},{"key":"7_CR8","unstructured":"Azure blockchain content and samples (2018). https:\/\/github.com\/Azure-Samples\/blockchain"},{"key":"7_CR9","unstructured":"Azure blockchain workbench (2018). https:\/\/azure.microsoft.com\/en-us\/features\/blockchain-workbench\/"},{"key":"7_CR10","unstructured":"Manticore (2018). https:\/\/github.com\/trailofbits\/manticore"},{"key":"7_CR11","unstructured":"Mythril classic: Security analysis tool for ethereum smart contracts (2018). https:\/\/github.com\/ConsenSys\/mythril-classic"},{"key":"7_CR12","unstructured":"Slither, the solidity source analyzer (2018). https:\/\/github.com\/trailofbits\/slither"},{"key":"7_CR13","unstructured":"Verisol: A formal verifier and analysis tool for solidity smart contracts (2018). https:\/\/github.com\/Microsoft\/verisol"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","volume-title":"Principles of Security and Trust","author":"N Atzei","year":"2017","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, 24 October 2016, pp. 91\u201396 (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500\u2013517. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45251-6_29"},{"issue":"OOPSLA","key":"7_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3276486","volume":"2","author":"Neville Grech","year":"2018","unstructured":"Grech, N., Kong, M., Jurisevic, A., Brent, L., Scholz, B., Smaragdakis, Y.: MadMax: surviving out-of-gas conditions in ethereum smart contracts. PACMPL 2(OOPSLA), 116:1\u2013116:27 (2018)","journal-title":"Proceedings of the ACM on Programming Languages"},{"issue":"POPL","key":"7_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158136","volume":"2","author":"Shelly Grossman","year":"2018","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2(POPL), 48:1\u201348:28 (2018)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the ethereum virtual machine. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9\u201312 July 2018, pp. 204\u2013217 (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, 18\u201321 February 2018 (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-02959-2_18","volume-title":"Automated Deduction \u2013 CADE-22","author":"SK Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S.: Complexity and algorithms for monomial and clausal predicate abstraction. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 214\u2013229. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_18"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 493\u2013508. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_37"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","volume-title":"Computer Aided Verification","author":"A Lal","year":"2012","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427\u2013443. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_32"},{"key":"7_CR25","unstructured":"Rustan, K., Leino, M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24\u201328 October 2016, pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Laszka, A.: Tool demonstration: Fsolidm for designing secure ethereum smart contracts. In: Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, 14\u201320 April 2018, Proceedings, pp. 270\u2013277 (2018)","DOI":"10.1007\/978-3-319-89722-6_11"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, 03\u201307 December 2018, pp. 653\u2013663 (2018)","DOI":"10.1145\/3274694.3274743"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Tsankov, P., et al.: Securify: practical security analysis of smart contracts. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15\u201319 October 2018, pp. 67\u201382 (2018)","DOI":"10.1145\/3243734.3243780"},{"key":"7_CR30","unstructured":"Wang, Y., et al.: Formal specification and verification of smart contracts in azure blockchain (2018). https:\/\/arxiv.org\/abs\/1812.08829\/"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-41600-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,3]],"date-time":"2021-03-03T22:44:59Z","timestamp":1614811499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-41600-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030415990","9783030416003"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-41600-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 March 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sri-csl.github.io\/VSTTE19\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}