Βιβλιοθήκη ΟΠΑ - Ψηφιακό Αποθετήριο

ΠΥΞΙΔΑ Ιδρυματικό Αποθετήριο
και Ψηφιακή Βιβλιοθήκη

Όνομα χρήστη
Κωδικός πρόσβασης

Συλλογές :	Ιδρυματικό Αποθετήριο ΟΠΑ / AUEB Institutional Repository Σχολή Επιστημών και Τεχνολογίας της Πληροφορίας / School of Informatics Τμήμα Πληροφορικής / Department of Informatics Μεταπτυχιακές Εργασίες / Postgraduate dissertations

Τίτλος :	Blockchain-based algorithmic problem solving competitions

Εναλλακτικός τίτλος :	Πλατφόρμα διεξαγωγής διαγωνισμών αλγοριθμικών προβλημάτων βασισμένη σε αλυσίδες καταχωρίσεων

Δημιουργός :	Aliprantis, Efstathios Αλιπράντης, Ευστάθιος

Συντελεστής :	Φουστούκου, Ευγενία (Επιβλέπων καθηγητής) Voulgaris, Spyridon (Εξεταστής) Markakis, Evangelos (Εξεταστής) Athens University of Economics and Business, Department of Informatics (Degree granting institution)

Τύπος :	Text

Φυσική περιγραφή :	98σ.

Γλώσσα :	en

Αναγνωριστικό :	http://www.pyxida.aueb.gr/index.php?op=view_object&object_id=9004

Περίληψη :	This thesis presents a blockchain-based platform where algorithmic problems can be posedas competitions, potentially, with a financial reward. A competition is won by the firstindividual to submit an algorithm that is both correct and bounded on time and spacecomplexity, in accordance with the specification of the corresponding problem. Submittedalgorithms must be accompanied by a formal proof of correctness which is mechanicallyvalidated by the platform. The platform is based on blockchain technology, specificallyEthereum, which ensures transparency on solution validation and allows for the automaticpayment of competition rewards.A complete system design is proposed and experimentally evaluated. The system consists ofa web-based front end and a blockain-based backend. The blockain-based backend conductscompetitions transparently and validates submitted algorithms and proofs mechanically. Theproposed system design is evaluated by an experimental proof-of-concept implementation.Furthermore, a theoretical setup is established in order to develop the methods and toolsrequired to make the platform a reality. This theoretical setup includes a method for theformal specification of computational problems where problem specifications are formattedas special problem-definition algorithms. A method for proving algorithm correctnessagainst such problem specifications is proposed based on formal program verification. Anew programming language with a fully working compiler is developed for the representationof algorithms. A proof composer for proofs of algorithm correctness is developed based ona custom configuration of Hoare logic. Η παρούσα διπλωματική εργασία παρουσιάζει μια πλατφόρμα στην οποία μπορούν ναδιεξαχθούν διαγωνισμοί για την επίλυση αλγοριθμικών προβλημάτων, προαιρετικά,με χρηματικό έπαθλο. Νικήτρια ενός διαγωνισμού ανακηρύσσεται η πρώτη συμμετοχήπου κρίνεται ορθή και ταυτόχρονα φράσσεται ως προς τη χρονική και χωρική πολυ-πλοκότητά της, βάσει των προδιαγραφών του υπό εξέταση αλγοριθμικού προβλήμα-τος. Οι συμμετοχές αποτελούνται έναν αλγόριθμο-επιλυτή καθώς και μία απόδειξηορθότητάς του, η οποία επαληθεύεται μηχανικά από την πλατφόρμα. Η πλατφόρμαβασίζεται σε τεχνολογία blockchain, συγκεκριμένα στο δίκτυο Ethereum, εξασφαλί-ζοντας διαφάνεια στην αξιολόγηση των συμμετοχών και επιτρέποντας την αυτόματηπληρωμή των χρηματικών επάθλων.Η εργασία προτείνει και αξιολογεί πειραματικά μια πλήρη σχεδίαση συστήματος. Τοσύστημα αποτελείται από μία διαδικτυακή διεπαφή και από ένα backend βασισμένοστο blockchain. Το backend είναι υπεύθυνο για τη διαφανή και αυτοματοποιημένηδιεξαγωγή των διαγωνισμών καθώς και για την μηχανική επικύρωση των υποβαλλό-μενων αλγορίθμων και αποδείξεων ορθότητας. Η προτεινόμενη σχεδίαση συστήματοςαξιολογείται πειραματικά μέσω μια βασικής υλοποίησης.Η εργασία, επίσης, εγκαθιδρύει μια θεωρητική βάση που καθιστά δυνατή την ανάπ-τυξη των απαραίτητων μεθόδων και εργαλείων ώστε να μπορέσει η πλατφόρμα ναγίνει πραγματικότητα. Η θεωρητική αυτή βάση περιλαμβάνει μια μέθοδο για τοντυπικό ορισμό των προδιαγραφών ενός υπολογιστικού προβλήματος σύμφωνα με τηνοποία ένα υπολογιστικό πρόβλημα παρίσταται από έναν ειδικό αλγόριθμο-ορισμό.Συνακολούθως, αναπτύσσεται μια μέθοδος για την απόδειξη της ορθότητας αλγο-ρίθμων σύμφωνα με τέτοιες τυπικά δοσμένες προδιαγραφές προβλημάτων. Μία νέαγλώσσα προγραμματισμού έχει σχεδιαστεί για το σκοπό της αναπαράσταση των αλ-γορίθμων. Η νέα αυτή γλώσσα συνοδεύεται από έναν πλήρως λειτουργικό compilerΕπιπλέον, έχει αναπτυχθεί ένας βοηθός σύνθεσης αποδείξεων ορθότητας αλγορίθμωνμε βάση μια προσαρμοσμένη διαμόρφωση της λογικής Hoare.

Περίληψη :

This thesis presents a blockchain-based platform where algorithmic problems can be posedas competitions, potentially, with a financial reward. A competition is won by the firstindividual to submit an algorithm that is both correct and bounded on time and spacecomplexity, in accordance with the specification of the corresponding problem. Submittedalgorithms must be accompanied by a formal proof of correctness which is mechanicallyvalidated by the platform. The platform is based on blockchain technology, specificallyEthereum, which ensures transparency on solution validation and allows for the automaticpayment of competition rewards.A complete system design is proposed and experimentally evaluated. The system consists ofa web-based front end and a blockain-based backend. The blockain-based backend conductscompetitions transparently and validates submitted algorithms and proofs mechanically. Theproposed system design is evaluated by an experimental proof-of-concept implementation.Furthermore, a theoretical setup is established in order to develop the methods and toolsrequired to make the platform a reality. This theoretical setup includes a method for theformal specification of computational problems where problem specifications are formattedas special problem-definition algorithms. A method for proving algorithm correctnessagainst such problem specifications is proposed based on formal program verification. Anew programming language with a fully working compiler is developed for the representationof algorithms. A proof composer for proofs of algorithm correctness is developed based ona custom configuration of Hoare logic.
Η παρούσα διπλωματική εργασία παρουσιάζει μια πλατφόρμα στην οποία μπορούν ναδιεξαχθούν διαγωνισμοί για την επίλυση αλγοριθμικών προβλημάτων, προαιρετικά,με χρηματικό έπαθλο. Νικήτρια ενός διαγωνισμού ανακηρύσσεται η πρώτη συμμετοχήπου κρίνεται ορθή και ταυτόχρονα φράσσεται ως προς τη χρονική και χωρική πολυ-πλοκότητά της, βάσει των προδιαγραφών του υπό εξέταση αλγοριθμικού προβλήμα-τος. Οι συμμετοχές αποτελούνται έναν αλγόριθμο-επιλυτή καθώς και μία απόδειξηορθότητάς του, η οποία επαληθεύεται μηχανικά από την πλατφόρμα. Η πλατφόρμαβασίζεται σε τεχνολογία blockchain, συγκεκριμένα στο δίκτυο Ethereum, εξασφαλί-ζοντας διαφάνεια στην αξιολόγηση των συμμετοχών και επιτρέποντας την αυτόματηπληρωμή των χρηματικών επάθλων.Η εργασία προτείνει και αξιολογεί πειραματικά μια πλήρη σχεδίαση συστήματος. Τοσύστημα αποτελείται από μία διαδικτυακή διεπαφή και από ένα backend βασισμένοστο blockchain. Το backend είναι υπεύθυνο για τη διαφανή και αυτοματοποιημένηδιεξαγωγή των διαγωνισμών καθώς και για την μηχανική επικύρωση των υποβαλλό-μενων αλγορίθμων και αποδείξεων ορθότητας. Η προτεινόμενη σχεδίαση συστήματοςαξιολογείται πειραματικά μέσω μια βασικής υλοποίησης.Η εργασία, επίσης, εγκαθιδρύει μια θεωρητική βάση που καθιστά δυνατή την ανάπ-τυξη των απαραίτητων μεθόδων και εργαλείων ώστε να μπορέσει η πλατφόρμα ναγίνει πραγματικότητα. Η θεωρητική αυτή βάση περιλαμβάνει μια μέθοδο για τοντυπικό ορισμό των προδιαγραφών ενός υπολογιστικού προβλήματος σύμφωνα με τηνοποία ένα υπολογιστικό πρόβλημα παρίσταται από έναν ειδικό αλγόριθμο-ορισμό.Συνακολούθως, αναπτύσσεται μια μέθοδος για την απόδειξη της ορθότητας αλγο-ρίθμων σύμφωνα με τέτοιες τυπικά δοσμένες προδιαγραφές προβλημάτων. Μία νέαγλώσσα προγραμματισμού έχει σχεδιαστεί για το σκοπό της αναπαράσταση των αλ-γορίθμων. Η νέα αυτή γλώσσα συνοδεύεται από έναν πλήρως λειτουργικό compilerΕπιπλέον, έχει αναπτυχθεί ένας βοηθός σύνθεσης αποδείξεων ορθότητας αλγορίθμωνμε βάση μια προσαρμοσμένη διαμόρφωση της λογικής Hoare.

Λέξη κλειδί :	Τυπικές αποδείξεις Αλγόριθμοι Διαγωνισμοί Αλυσίδες καταχωρίσεων Επαλήθευση λογισμικού Formal proofs Algorithms Competitions Blockchains Program verification

Διαθέσιμο από :	2022-01-01 22:22:27

Ημερομηνία έκδοσης :	2021

Ημερομηνία κατάθεσης :	2022-01-01 22:22:27

Δικαιώματα χρήσης :	Free access

Άδεια χρήσης :

Αρχείο: Aliprantis_2021.pdf

Τύπος: application/pdf

Είσοδος