Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15470
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Μιχαήλ Γιακκούπης | |
dc.date.accessioned | 2018-07-23T15:56:39Z | - |
dc.date.available | 2018-07-23T15:56:39Z | - |
dc.date.issued | 2009-7-23 | |
dc.date.submitted | 2009-12-20 | |
dc.identifier.uri | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15470 | - |
dc.description.abstract | Σκοπός της εργασίας αυτής είναι η τυπική επαλήθευση της λύσης ενός προβλήματος παρόμοιου με τα προβλημάτα που εξετάζονται στην Ολυμπιάδα Πληροφορικής. Η τυπική επαλήθευση ενός προγράμματος αποτελεί τη διαδικασία απόδειξης ορθότητας του προγράμματος με βάση κάποια τυπικήπροδιαγραφή ή ιδιότητα, χρησιμοποιώντας ως εργαλεία τυπικές μεθόδους και μαθηματική λογική.Στην περίπτωσή μας υλοποιήσαμε μία λύση για το πρόβλημα με τίτλο damage2, που ήταν ένα από τα θέματα του διαγωνισμού πληροφορικής του Μαρτίου 2009 της USACO. Το πρόβλημα αυτόανάγεται εύκολα στο γνωστό από τη θεωρία γράφων πρόβλημα της εύρεσης ελάχιστης τομής (min cut) γράφου χωρίς βάρη, για τη λύση του οποίου μπορεί να χρησιμοποιηθεί ο αλγόριθμος των Ford-Fulkerson, Στη συνέχεια αποδείξαμε την ορθότητα της υλοποίησης αυτού του αλγορίθμου σε γλώσσαC, χρησιμοποιώντας τα εργαλεία Caduceus και Coq. | |
dc.language | Greek | |
dc.subject | αλγόριθμος ford-fulkerson | |
dc.subject | πρόβλημα μέγιστης ροής/ ελάχιστης τομής | |
dc.subject | απόδειξη ορθότητας | |
dc.subject | πρόβλημα damage2 από usaco | |
dc.subject | coq. | |
dc.title | Απόδειξη Ορθότητας Μίας Υλοποίησης Του Αλγορίθμου Των Ford-fulkerson Για Την Εύρεση Της Ελάχιστης Τομής Γράφου Χωρίς Βάρη | |
dc.type | Diploma Thesis | |
dc.description.pages | 45 | |
dc.contributor.supervisor | Παπασπύρου Νικόλαος | |
dc.department | Τομέας Τεχνολογίας Πληροφορικής & Υπολογιστών | |
dc.organization | ΕΜΠ, Τμήμα Ηλεκτρολόγων Μηχανικών & Μηχανικών Υπολογιστών | |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
DT2009-0207.pdf | 1.46 MB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.