Ο φοιτητής του προγράμματος Κυριάκος Παπαδόπουλος θα παρουσιάσει τη διπλωματική του εργασία με θέμα:
Outline of a concurrent dynamic deontic logic for the specification of Smart Contracts
τη Δευτέρα 21 Ιουλίου 2025 και ώρα 18:00, διαδικτυακά https://meet.google.com/hng-ptmt-dco).
Σύνοψη Διπλωματικής:
The blockchain technology has taken the computing world by storm and seems to revolutionize several application areas in many important respects. A tool that lies at the heart of this revolution is the smart contract. Smart Contracts (SCs) are specialized programs residing on a blockchain, functioning as digital contracts (in the sense of automating the execution of agreements) and eliminating the need for mutual trust, regulatory authorities and intermediaries. Smart Contracts are immutable and so are their consequences in the distributed ledger. They also possess a complicated execution model, not easily amenable to a formal specification: they receive data from external sources, they can recurrently call each other and their execution depends on blockchain resources (the gas). Smart contracts have opened the door to a brave new world of digital assets and online financial transactions. This world is extremely fascinating and technologically challenging but very dangerous too; the several infamous hacks that have resulted in huge financial losses witness this statement. It is now widely understood that SCs are safety-critical applications and there is a striking need for tools and techniques to assist in their formal verification. The existing model checking techniques - which represent a remarkable success story and allow for the verification of protocols with an immense number of states - do not suffice; the literature includes convincing arguments on this. We argue that a prime candidate for specifying and verifying SCs should be a non-classical logic that combines dynamic deontic principles, temporal expressibility and (sort of) concurrency handling in the form of identifying and checking callbacks. This is a highly non-trivial project: smart contracts are complex entities that should encode legal concepts (obligations, permissions, rewards, penalties), temporal concepts (deadlines, extensions, grace periods) and (ideally) calendar milestones (dates, durations), along with a way to handle the notoriously complex execution model (calling external objects, concurrent access to resources, recursive calls between contracts). We survey the deontic, the temporal and the ‘concurrent’ perspective on smart contracts and outline a dynamic deontic concurrent logic for this purpose.
Η επιτροπή,
Κώστας Κούτρας (Επιβλέπων),
Αναπληρωτής Καθηγητής AUM
Παναγιώτης Ροντογιάννης (Συνεπιβλέπων),
Τμήμα Πληροφορικής, Ε.Κ.Π.Α.
Νικόλαος Ρήγας,
Εξωτερικός συνεργάτης