Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq
المؤلفون المشاركون
المصدر
Mathematical Problems in Engineering
العدد
المجلد 2020، العدد 2020 (31 ديسمبر/كانون الأول 2020)، ص ص. 1-15، 15ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2020-12-01
دولة النشر
مصر
عدد الصفحات
15
التخصصات الرئيسية
الملخص EN
The security of blockchain smart contracts is one of the most emerging issues of the greatest interest for researchers.
This article presents an intermediate specification language for the formal verification of Ethereum-based smart contract in Coq, denoted as Lolisa.
The formal syntax and semantics of Lolisa contain a large subset of the Solidity programming language developed for the Ethereum blockchain platform.
To enhance type safety, the formal syntax of Lolisa adopts a stronger static type system than Solidity.
In addition, Lolisa includes a large subset of Solidity syntax components as well as general-purpose programming language features.
Therefore, Solidity programs can be directly translated into Lolisa with line-by-line correspondence.
Lolisa is inherently generalizable and can be extended to express other programming languages.
Finally, the syntax and semantics of Lolisa have been encapsulated as an interpreter in mathematical tool Coq.
Hence, smart contracts written in Lolisa can be symbolically executed and verified in Coq.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Yang, Zheng& Lei, Hang. 2020. Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq. Mathematical Problems in Engineering،Vol. 2020, no. 2020, pp.1-15.
https://search.emarefa.net/detail/BIM-1196576
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Yang, Zheng& Lei, Hang. Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq. Mathematical Problems in Engineering No. 2020 (2020), pp.1-15.
https://search.emarefa.net/detail/BIM-1196576
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Yang, Zheng& Lei, Hang. Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq. Mathematical Problems in Engineering. 2020. Vol. 2020, no. 2020, pp.1-15.
https://search.emarefa.net/detail/BIM-1196576
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-1196576
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر