Μονάδα:
Κατεύθυνση / ειδίκευση Υπολογιστικά Συστήματα: Λογισμικό και Υλικό (ΣΥΣ)Πληροφορική
Ημερομηνία κατάθεσης:
2019-10-22
Συγγραφέας:
Βραχάς Χρίστος
Στοιχεία επιβλεπόντων καθηγητών:
Σμαραγδάκης Γιάννης, Καθηγητής, Πληροφορικής και Τηλεπικοινωνιών, Εθνικό και Καποδιστριακό Πανεπιστήμιο Αθηνών
Πρωτότυπος Τίτλος:
Datalog Based Symbolic Program Reasoning for Java
Γλώσσες εργασίας:
Αγγλικά
Μεταφρασμένος τίτλος:
Συμβολική Συλλογιστική Προγραμμάτων για Java, βασισμένη σε Datalog
Περίληψη:
Έχοντας ως κίνητρο την επιτυχία των προγραμμάτων απόδειξης θεωρημάτων ως υποστηρικτικά εργαλεία στην συμβολική εκτέλεση και την ευκολία που παρέχουν οι δηλωτικές
γλώσσες προγραμματισμού, στην εργασία αυτή επιχειρούμε να εισάγουμε μια αυστηρώς
δηλωτική υλοποίηση ενός προγράμματος απόδειξης θεωρημάτων σε Datalog. Η προσέγγισή μας, πιο συγκεκριμένα η στατικά δηλωτική συμβολική συλλογιστική, υλοποιήθηκε
στα πλαίσια του εργαλείου Doop για Ανάλυση Δεικτών σε προγράμματα Java, και κυρίως
επιδιώκει να δώσει απάντηση στο ”Ποιες είναι οι εκφράσεις οι οποίες συνεπάγονται από
άλλες εκφράσεις εντός ενός προγράμματος”. Το κύριο κίνητρο πίσω από αυτήν την απόφαση ήταν η αξιοποίηση των ισχυρών δομών του Doop και ταυτόχρονα η παροχή της δυνατότητας μελλοντικής χρησιμοποίησης του εργαλείου συλλογιστικής στο μέλλον.
Κύρια θεματική κατηγορία:
Τεχνολογία – Πληροφορική
Λέξεις-κλειδιά:
”ευαισθησία”-ροής, ”ευαισθησία”-μονοπατιού, κανόνες συμπερασμού και αποδείξεις προτασιακής λογικής
Αρ. σελίδων ευρετηρίου:
5
Αρ. βιβλιογραφικών αναφορών:
18
