| CODE | DLT5402 | ||||||||
| TITLE | Verification Techniques for Smart Contracts | ||||||||
| UM LEVEL | 05 - Postgraduate Modular Diploma or Degree Course | ||||||||
| MQF LEVEL | 7 | ||||||||
| ECTS CREDITS | 5 | ||||||||
| DEPARTMENT | Centre for Distributed Ledger Technologies | ||||||||
| DESCRIPTION | This study-unit covers techniques for the verification of smart contracts, in particular focussing on Ethereum ones (although the techniques can be readily applied to other blockchain systems). The unit consists of four parts: 1. Specification techniques: This will introduce students to how to identify and specify properties of smart contracts, allowing for verification techniques to be applied; 2. Testing: The students will be introduced to testing, with an emphasis on smart contracts. The course will cover standard topics from testing (e.g. the writing of unit tests, test suites, coverage analysis, etc.) but with a slant for smart contracts, enabling also non-functional profiling/testing for gas consumption and other features. The unit will also cover smart contract design in tandem with a testing strategy in order to maximise testing coverage of functional requirements; 3. Runtime verification: The students will be introduced to the basics of runtime verification and use tools to integrate runtime tests to their smart contracts; 4. Static analysis: Finally students will be given an overview of static analysis techniques and tools for smart contracts. The assessment is fully assignment-based, but students may be called in for an interview. Study-unit Aims: The main aims of the unit are to: 1. Expose students to real-life applications of verification techniques and tools for smart contracts; 2. Enable students to understand a smart contract's requirements and formulate them in an appropriate notation; 3. Appreciate different software verification techniques and understand when to apply them. Learning Outcomes: 1. Knowledge & Understanding By the end of the study-unit the student will be able to: - Compare different concepts and approaches in software verification, particularly for smart contracts on blockchain/DLT platforms; - Contrast and describe the differences, advantages and disadvantages of various verification techniques; - Reason with appropriate notation about the requirements of a smart contract, increasing confidence in its correctness. 2. Skills By the end of the study-unit the student will be able to: - Identify, document and analyse the requirements of a smart contracts using one of a number of specification formalisms; - Apply a number of software verification techniques to smart contracts in Solidity and on Ethereum; - Choose the appropriate verification technique for a given software verification requirement; - Use standard tools for smart contract quality assurance, including executing testing strategies in a sandbox environment; - Factor in testing strategies in the architecture phase of the smart contract to ensure that it can be fully tested to satisfy the required criteria. Main Text/s and any supplementary readings: - Mastering Ethereum: Building Smart Contracts and DApps. Andreas M. Antonopoulos and Gavin Wood. O'Reilly, 2018. ISBN 1491971940. - Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, ISBN: 978-0262032704, M.I.T. Press, 1999. ISBN 0262032708. - Lectures on Runtime Verification: Introductory and Advanced Topics, Ezio Bartocci, Ylies Falcone (editors), Springer, 2018. ISBN 978-3-319-75632-5. Additional reading material will be provided to the students through a number of key-papers in the area. |
||||||||
| ADDITIONAL NOTES | Co-Requisite Study-unit: DLT5401 | ||||||||
| STUDY-UNIT TYPE | Lecture and Independent Study | ||||||||
| METHOD OF ASSESSMENT |
|
||||||||
| LECTURER/S | Wolfgang Ahrendt Shaun Paul Azzopardi Mark Mallia |
||||||||
|
The University makes every effort to ensure that the published Courses Plans, Programmes of Study and Study-Unit information are complete and up-to-date at the time of publication. The University reserves the right to make changes in case errors are detected after publication.
The availability of optional units may be subject to timetabling constraints. Units not attracting a sufficient number of registrations may be withdrawn without notice. It should be noted that all the information in the description above applies to study-units available during the academic year 2023/4. It may be subject to change in subsequent years. |
|||||||||